Theorem prnzg 4722

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2932  ∅c0 4273  {cpr 4569

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-pr 4570

This theorem is referenced by:  preqsnd  4802  0nelop  5450  fr2nr  5608  mreincl  17561  subrngin  20538  subrgin  20573  lssincl  20960  incld  23008  umgrnloopv  29175  upgr1elem  29181  usgrnloopvALT  29270  difelsiga  34277  inelpisys  34298  inidl  38351  coss0  38890  pmapmeet  40219  diameetN  41502  dihmeetlem2N  41745  dihmeetcN  41748  dihmeet  41789  infsubc  49535  infsubc2  49536