Theorem prnzg 4711

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

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2934  ∅c0 4262  {cpr 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-v 3433  df-dif 3886  df-un 3888  df-nul 4263  df-sn 4557  df-pr 4559

This theorem is referenced by:  preqsnd  4791  0nelop  5438  fr2nr  5596  mreincl  17553  subrngin  20534  subrgin  20569  lssincl  20956  incld  23027  umgrnloopv  29194  upgr1elem  29200  usgrnloopvALT  29289  difelsiga  34326  inelpisys  34347  inidl  38406  coss0  38945  pmapmeet  40274  diameetN  41557  dihmeetlem2N  41800  dihmeetcN  41803  dihmeet  41844  infsubc  49558  infsubc2  49559