Theorem prnzg 4739

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591

This theorem is used by:  preqsnd  4817  0nelop  5472  fr2nr  5632  mreincl  17795  subrngin  20840  subrgin  20875  lssincl  21267  incld  23388  umgrnloopv  29711  upgr1elem  29717  usgrnloopvALT  29809  inlidl  34038  inelpisys  34854  inidl  39155  coss0  39692  pmapmeet  41021  diameetN  42304  dihmeetlem2N  42547  dihmeetcN  42550  dihmeet  42591  infsubc  50377  infsubc2  50378