Theorem prnzg 4733

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930  ∅c0 4283  {cpr 4580

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-v 3440  df-dif 3902  df-un 3904  df-nul 4284  df-sn 4579  df-pr 4581

This theorem is referenced by:  preqsnd  4813  0nelop  5442  fr2nr  5599  mreincl  17516  subrngin  20492  subrgin  20527  lssincl  20914  incld  22985  umgrnloopv  29128  upgr1elem  29134  usgrnloopvALT  29223  difelsiga  34239  inelpisys  34260  inidl  38170  coss0  38681  pmapmeet  39972  diameetN  41255  dihmeetlem2N  41498  dihmeetcN  41501  dihmeet  41542  infsubc  49247  infsubc2  49248