Theorem prnzg 4672

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

Syntax hints:   → wi 4   ∈ wcel 2112   ≠ wne 2952  ∅c0 4226  {cpr 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ne 2953  df-v 3412  df-dif 3862  df-un 3864  df-nul 4227  df-sn 4524  df-pr 4526

This theorem is referenced by:  preqsnd  4747  0nelop  5356  fr2nr  5503  mreincl  16921  subrgin  19619  lssincl  19798  incld  21736  umgrnloopv  26991  upgr1elem  26997  usgrnloopvALT  27083  difelsiga  31613  inelpisys  31634  inidl  35741  coss0  36152  pmapmeet  37342  diameetN  38625  dihmeetlem2N  38868  dihmeetcN  38871  dihmeet  38912