Theorem prnzg 4783

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

Syntax hints:   → wi 4   ∈ wcel 2099   ≠ wne 2937  ∅c0 4323  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3473  df-dif 3950  df-un 3952  df-nul 4324  df-sn 4630  df-pr 4632

This theorem is referenced by:  preqsnd  4860  0nelop  5498  fr2nr  5656  mreincl  17578  subrngin  20497  subrgin  20534  lssincl  20848  incld  22946  umgrnloopv  28918  upgr1elem  28924  usgrnloopvALT  29013  difelsiga  33752  inelpisys  33773  inidl  37503  coss0  37951  pmapmeet  39246  diameetN  40529  dihmeetlem2N  40772  dihmeetcN  40775  dihmeet  40816