Theorem prnzg 4715

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 3018  ∅c0 4293  {cpr 4571

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-v 3498  df-dif 3941  df-un 3943  df-nul 4294  df-sn 4570  df-pr 4572

This theorem is referenced by:  preqsnd  4791  0nelop  5388  fr2nr  5535  mreincl  16872  subrgin  19560  lssincl  19739  incld  21653  umgrnloopv  26893  upgr1elem  26899  usgrnloopvALT  26985  difelsiga  31394  inelpisys  31415  inidl  35310  coss0  35721  pmapmeet  36911  diameetN  38194  dihmeetlem2N  38437  dihmeetcN  38440  dihmeet  38481