Theorem prnzg 4745

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 4727	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐵})
2	1	ne0d 4308	1 ⊢ (𝐴 ∈ 𝑉 → {𝐴, 𝐵} ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2926  ∅c0 4299  {cpr 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-nul 4300  df-sn 4593  df-pr 4595

This theorem is referenced by:  preqsnd  4826  0nelop  5459  fr2nr  5618  mreincl  17567  subrngin  20477  subrgin  20512  lssincl  20878  incld  22937  umgrnloopv  29040  upgr1elem  29046  usgrnloopvALT  29135  difelsiga  34130  inelpisys  34151  inidl  38031  coss0  38477  pmapmeet  39774  diameetN  41057  dihmeetlem2N  41300  dihmeetcN  41303  dihmeet  41344  infsubc  49053  infsubc2  49054