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

Theorem prnzg 4712
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 4695 . 2 (𝐴𝑉𝐴 ∈ {𝐴, 𝐵})
21ne0d 4305 1 (𝐴𝑉 → {𝐴, 𝐵} ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 3021  c0 4295  {cpr 4566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-v 3502  df-dif 3943  df-un 3945  df-nul 4296  df-sn 4565  df-pr 4567
This theorem is referenced by:  preqsnd  4788  0nelop  5383  fr2nr  5532  mreincl  16860  subrgin  19478  lssincl  19657  incld  21567  umgrnloopv  26805  upgr1elem  26811  usgrnloopvALT  26897  difelsiga  31278  inelpisys  31299  inidl  35176  coss0  35586  pmapmeet  36776  diameetN  38059  dihmeetlem2N  38302  dihmeetcN  38305  dihmeet  38346
  Copyright terms: Public domain W3C validator