MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prnzg Structured version   Unicode version

Theorem prnzg 4147
Description: A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.)
Assertion
Ref Expression
prnzg  |-  ( A  e.  V  ->  { A ,  B }  =/=  (/) )

Proof of Theorem prnzg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 preq1 4106 . . 3  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
21neeq1d 2744 . 2  |-  ( x  =  A  ->  ( { x ,  B }  =/=  (/)  <->  { A ,  B }  =/=  (/) ) )
3 vex 3116 . . 3  |-  x  e. 
_V
43prnz 4146 . 2  |-  { x ,  B }  =/=  (/)
52, 4vtoclg 3171 1  |-  ( A  e.  V  ->  { A ,  B }  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767    =/= wne 2662   (/)c0 3785   {cpr 4029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-sn 4028  df-pr 4030
This theorem is referenced by:  0nelop  4737  fr2nr  4857  mreincl  14847  subrgin  17232  lssincl  17391  incld  19307  umgra1  23999  uslgra1  24045  usgranloopv  24051  difelsiga  27770  inidl  30028  pmapmeet  34569  diameetN  35853  dihmeetlem2N  36096  dihmeetcN  36099  dihmeet  36140
  Copyright terms: Public domain W3C validator