Theorem prnzg 4737

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

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

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 3444  df-dif 3906  df-un 3908  df-nul 4288  df-sn 4583  df-pr 4585

This theorem is referenced by:  preqsnd  4817  0nelop  5452  fr2nr  5609  mreincl  17530  subrngin  20509  subrgin  20544  lssincl  20931  incld  23002  umgrnloopv  29195  upgr1elem  29201  usgrnloopvALT  29290  difelsiga  34315  inelpisys  34336  inidl  38285  coss0  38824  pmapmeet  40153  diameetN  41436  dihmeetlem2N  41679  dihmeetcN  41682  dihmeet  41723  infsubc  49423  infsubc2  49424