Theorem prnzg 4723

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

Step	Hyp	Ref	Expression
1		prid1g 4705	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
2	1	ne0d 4283	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-un 3895  df-nul 4275  df-sn 4569  df-pr 4571

This theorem is referenced by:  preqsnd  4803  0nelop  5446  fr2nr  5603  mreincl  17556  subrngin  20533  subrgin  20568  lssincl  20955  incld  23022  umgrnloopv  29193  upgr1elem  29199  usgrnloopvALT  29288  difelsiga  34297  inelpisys  34318  inidl  38369  coss0  38908  pmapmeet  40237  diameetN  41520  dihmeetlem2N  41763  dihmeetcN  41766  dihmeet  41807  infsubc  49551  infsubc2  49552