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

Theorem prnzg 4705
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 4688 . 2 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
21ne0d 4298 1 (𝐴𝑉 → {𝐴, 𝐵} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wne 3013  c0 4288  {cpr 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-v 3494  df-dif 3936  df-un 3938  df-nul 4289  df-sn 4558  df-pr 4560
This theorem is referenced by:  preqsnd  4781  0nelop  5377  fr2nr  5526  mreincl  16858  subrgin  19487  lssincl  19666  incld  21579  umgrnloopv  26818  upgr1elem  26824  usgrnloopvALT  26910  difelsiga  31291  inelpisys  31312  inidl  35189  coss0  35599  pmapmeet  36789  diameetN  38072  dihmeetlem2N  38315  dihmeetcN  38318  dihmeet  38359
  Copyright terms: Public domain W3C validator