Theorem prnzg 4739

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

Syntax hints:   → wi 4   ∈ wcel 2144   ≠ wne 2959  ∅c0 4287  {cpr 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-v 3458  df-dif 3909  df-un 3911  df-nul 4288  df-sn 4585  df-pr 4587

This theorem is referenced by:  preqsnd  4819  0nelop  5467  fr2nr  5626  mreincl  17629  subrngin  20613  subrgin  20648  lssincl  21034  incld  23105  umgrnloopv  29309  upgr1elem  29315  usgrnloopvALT  29404  difelsiga  34432  inelpisys  34453  inidl  38534  coss0  39073  pmapmeet  40402  diameetN  41685  dihmeetlem2N  41928  dihmeetcN  41931  dihmeet  41972  infsubc  49686  infsubc2  49687