Theorem prnzg 4713

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

Syntax hints:   → wi 4   ∈ wcel 2121   ≠ wne 2936  ∅c0 4264  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-un 3890  df-nul 4265  df-sn 4559  df-pr 4561

This theorem is referenced by:  preqsnd  4793  0nelop  5440  fr2nr  5598  mreincl  17556  subrngin  20537  subrgin  20572  lssincl  20959  incld  23030  umgrnloopv  29197  upgr1elem  29203  usgrnloopvALT  29292  difelsiga  34329  inelpisys  34350  inidl  38412  coss0  38951  pmapmeet  40280  diameetN  41563  dihmeetlem2N  41806  dihmeetcN  41809  dihmeet  41850  infsubc  49564  infsubc2  49565