Theorem prnzg 4735

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2932  ∅c0 4285  {cpr 4582

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-sn 4581  df-pr 4583

This theorem is referenced by:  preqsnd  4815  0nelop  5444  fr2nr  5601  mreincl  17520  subrngin  20496  subrgin  20531  lssincl  20918  incld  22989  umgrnloopv  29181  upgr1elem  29187  usgrnloopvALT  29276  difelsiga  34292  inelpisys  34313  inidl  38233  coss0  38764  pmapmeet  40055  diameetN  41338  dihmeetlem2N  41581  dihmeetcN  41584  dihmeet  41625  infsubc  49326  infsubc2  49327