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

Theorem prnzg 4091
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 4050 . . 3  |-  ( x  =  A  ->  { x ,  B }  =  { A ,  B }
)
21neeq1d 2682 . 2  |-  ( x  =  A  ->  ( { x ,  B }  =/=  (/)  <->  { A ,  B }  =/=  (/) ) )
3 vex 3047 . . 3  |-  x  e. 
_V
43prnz 4090 . 2  |-  { x ,  B }  =/=  (/)
52, 4vtoclg 3106 1  |-  ( A  e.  V  ->  { A ,  B }  =/=  (/) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1443    e. wcel 1886    =/= wne 2621   (/)c0 3730   {cpr 3969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-un 3408  df-nul 3731  df-sn 3968  df-pr 3970
This theorem is referenced by:  0nelop  4690  fr2nr  4811  mreincl  15498  subrgin  18024  lssincl  18181  incld  20051  umgra1  25046  uslgra1  25092  usgranloopv  25098  difelsiga  28948  inelpisys  28969  inidl  32256  pmapmeet  33332  diameetN  34618  dihmeetlem2N  34861  dihmeetcN  34864  dihmeet  34905  umgrnloopv  39180  upgr1elem  39186  usgrnloopvALT  39270
  Copyright terms: Public domain W3C validator