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

Theorem prnzg 4106
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 4065 . . 3  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
21neeq1d 2729 . 2  |-  ( x  =  A  ->  ( { x ,  B }  =/=  (/)  <->  { A ,  B }  =/=  (/) ) )
3 vex 3081 . . 3  |-  x  e. 
_V
43prnz 4105 . 2  |-  { x ,  B }  =/=  (/)
52, 4vtoclg 3136 1  |-  ( A  e.  V  ->  { A ,  B }  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758    =/= wne 2648   (/)c0 3748   {cpr 3990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-un 3444  df-nul 3749  df-sn 3989  df-pr 3991
This theorem is referenced by:  0nelop  4692  fr2nr  4809  mreincl  14659  subrgin  17014  lssincl  17172  incld  18782  umgra1  23432  uslgra1  23463  usgranloopv  23469  difelsiga  26741  inidl  28998  pmapmeet  33775  diameetN  35059  dihmeetlem2N  35302  dihmeetcN  35305  dihmeet  35346
  Copyright terms: Public domain W3C validator