Theorem prnzg 4782

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2939  ∅c0 4322  {cpr 4630

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-v 3475  df-dif 3951  df-un 3953  df-nul 4323  df-sn 4629  df-pr 4631

This theorem is referenced by:  preqsnd  4859  0nelop  5496  fr2nr  5654  mreincl  17550  subrngin  20457  subrgin  20494  lssincl  20808  incld  22867  umgrnloopv  28800  upgr1elem  28806  usgrnloopvALT  28892  difelsiga  33596  inelpisys  33617  inidl  37364  coss0  37815  pmapmeet  39110  diameetN  40393  dihmeetlem2N  40636  dihmeetcN  40639  dihmeet  40680