Theorem prnzg 4728

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2928  ∅c0 4280  {cpr 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-nul 4281  df-sn 4574  df-pr 4576

This theorem is referenced by:  preqsnd  4808  0nelop  5434  fr2nr  5591  mreincl  17501  subrngin  20476  subrgin  20511  lssincl  20898  incld  22958  umgrnloopv  29084  upgr1elem  29090  usgrnloopvALT  29179  difelsiga  34146  inelpisys  34167  inidl  38080  coss0  38591  pmapmeet  39882  diameetN  41165  dihmeetlem2N  41408  dihmeetcN  41411  dihmeet  41452  infsubc  49171  infsubc2  49172