Theorem prex 2771

Description: The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc 2445), so we can dispense with hypotheses requiring them to be sets.

Assertion

Ref	Expression
prex	|- {A, B} e. V

Proof of Theorem prex

Step	Hyp	Ref	Expression
1		preq1 2438	. . . . 5 |- (x = A -> {x, B} = {A, B})
2	1	eleq1d 1532	. . . 4 |- (x = A -> ({x, B} e. V <-> {A, B} e. V))
3		preq2 2439	. . . . . 6 |- (y = B -> {x, y} = {x, B})
4	3	eleq1d 1532	. . . . 5 |- (y = B -> ({x, y} e. V <-> {x, B} e. V))
5		zfpair2 2770	. . . . 5 |- {x, y} e. V
6	4, 5	vtoclg 1838	. . . 4 |- (B e. V -> {x, B} e. V)
7	2, 6	syl5bi 208	. . 3 |- (x = A -> (B e. V -> {A, B} e. V))
8	7	vtocleg 1846	. 2 |- (A e. V -> (B e. V -> {A, B} e. V))
9		prprc1 2443	. . 3 |- (-. A e. V -> {A, B} = {B})
10		snex 2740	. . 3 |- {B} e. V
11	9, 10	syl6eqel 1548	. 2 |- (-. A e. V -> {A, B} e. V)
12		prprc2 2444	. . 3 |- (-. B e. V -> {A, B} = {A})
13		snex 2740	. . 3 |- {A} e. V
14	12, 13	syl6eqel 1548	. 2 |- (-. B e. V -> {A, B} e. V)
15	8, 11, 14	pm2.61nii 131	1 |- {A, B} e. V

Syntax hints:  -. wn 2   -> wi 3   = wceq 953   e. wcel 955  Vcvv 1802  {csn 2399  {cpr 2400

This theorem is referenced by:  opex 2772  opi2 2775  opth 2777  opeqsn 2791  opeqpr 2792  opthwiener 2796  uniop 2797  unex 2863  tpex 2868  op1stb 2903  xpsspw 3247  relop 3265  opthreg 4576  rankop 4665  aceq6b 4714  xrex 5464  unctb 7519  indistop 7590  cnfilca 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403

Copyright terms: Public domain