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

Proof of Theorem prnzg
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 preq1 4050 . . 3
21neeq1d 2682 . 2
3 vex 3047 . . 3
43prnz 4090 . 2
52, 4vtoclg 3106 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1443   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