Theorem prnzg 4744

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143   ≠ wne 2958  ∅c0 4286  {cpr 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4590  df-pr 4592

This theorem is used by:  preqsnd  4824  0nelop  5479  fr2nr  5638  mreincl  17655  subrngin  20669  subrgin  20704  lssincl  21095  incld  23209  umgrnloopv  29465  upgr1elem  29471  usgrnloopvALT  29560  inlidl  33738  difelsiga  34532  inelpisys  34553  inidl  38709  coss0  39246  pmapmeet  40575  diameetN  41858  dihmeetlem2N  42101  dihmeetcN  42104  dihmeet  42145  infsubc  49866  infsubc2  49867