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

Theorem prnzg 4465
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 4450 . 2 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
21ne0d 4086 1 (𝐴𝑉 → {𝐴, 𝐵} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wne 2937  c0 4079  {cpr 4336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-v 3352  df-dif 3735  df-un 3737  df-nul 4080  df-sn 4335  df-pr 4337
This theorem is referenced by:  preqsnd  4543  0nelop  5115  fr2nr  5255  mreincl  16527  subrgin  19072  lssincl  19237  incld  21127  umgrnloopv  26278  upgr1elem  26284  usgrnloopvALT  26371  difelsiga  30578  inelpisys  30599  inidl  34183  coss0  34590  pmapmeet  35661  diameetN  36944  dihmeetlem2N  37187  dihmeetcN  37190  dihmeet  37231
  Copyright terms: Public domain W3C validator