Theorem prnzg 4746

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960  ∅c0 4286  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-un 3911  df-nul 4287  df-sn 4592  df-pr 4594

This theorem is used by:  preqsnd  4826  0nelop  5481  fr2nr  5640  mreincl  17677  subrngin  20714  subrgin  20749  lssincl  21140  incld  23254  umgrnloopv  29515  upgr1elem  29521  usgrnloopvALT  29613  inlidl  33797  inelpisys  34613  inidl  38743  coss0  39280  pmapmeet  40609  diameetN  41892  dihmeetlem2N  42135  dihmeetcN  42138  dihmeet  42179  infsubc  49914  infsubc2  49915