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

Theorem prnzg 4672
 Description: A pair containing a set is not empty. (Contributed by FL, 19-Sep-2011.) (Proof shortened by JJ, 23-Jul-2021.)
Assertion
Ref Expression
prnzg (𝐴𝑉 → {𝐴, 𝐵} ≠ ∅)

Proof of Theorem prnzg
StepHypRef Expression
1 prid1g 4654 . 2 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
21ne0d 4235 1 (𝐴𝑉 → {𝐴, 𝐵} ≠ ∅)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2112   ≠ wne 2952  ∅c0 4226  {cpr 4525 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ne 2953  df-v 3412  df-dif 3862  df-un 3864  df-nul 4227  df-sn 4524  df-pr 4526 This theorem is referenced by:  preqsnd  4747  0nelop  5356  fr2nr  5503  mreincl  16921  subrgin  19619  lssincl  19798  incld  21736  umgrnloopv  26991  upgr1elem  26997  usgrnloopvALT  27083  difelsiga  31613  inelpisys  31634  inidl  35741  coss0  36152  pmapmeet  37342  diameetN  38625  dihmeetlem2N  38868  dihmeetcN  38871  dihmeet  38912
 Copyright terms: Public domain W3C validator