Theorem prnz 2471

Description: A pair containing a set is not empty.

Hypothesis

Ref	Expression
prnz.1	⊢ A ∈ V

Assertion

Ref	Expression
prnz	⊢ {A, B} ≠ ∅

Proof of Theorem prnz

Step	Hyp	Ref	Expression
1		prnz.1	. . 3 ⊢ A ∈ V
2	1	prid1 2462	. 2 ⊢ A ∈ {A, B}
3		ne0i 2295	. 2 ⊢ (A ∈ {A, B} → {A, B} ≠ ∅)
4	2, 3	ax-mp 7	1 ⊢ {A, B} ≠ ∅

Syntax hints:   ∈ wcel 962   ≠ wne 1592  Vcvv 1818  ∅c0 2289  {cpr 2420

This theorem is referenced by:  opprc1b 2810  fr2nr 2939  fiint 4570  shincl 9338  chincl 9390

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-12 972  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1178  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-v 1819  df-dif 2058  df-un 2059  df-nul 2290  df-sn 2422  df-pr 2423

Copyright terms: Public domain