Theorem prnzg 4749

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

Syntax hints:   → wi 4   ∈ wcel 2149   ≠ wne 2964  ∅c0 4294  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295  df-sn 4595  df-pr 4597

This theorem is referenced by:  preqsnd  4828  0nelop  5480  fr2nr  5639  mreincl  17651  subrngin  20646  subrgin  20681  lssincl  21064  incld  23169  umgrnloopv  29397  upgr1elem  29403  usgrnloopvALT  29492  inlidl  33673  difelsiga  34468  inelpisys  34489  inidl  38603  coss0  39142  pmapmeet  40471  diameetN  41754  dihmeetlem2N  41997  dihmeetcN  42000  dihmeet  42041  infsubc  49757  infsubc2  49758