Theorem opthprc 4334

Description: Justification theorem for an ordered pair definition that works for any classes, including proper classes. This is a possible definition implied by the footnote in [Jech] p. 78, which says, "The sophisticated reader will not object to our use of a pair of classes." (Contributed by NM, 28-Sep-2003.)

Assertion

Ref	Expression
opthprc	|- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) <-> (A = C /\ B = D))

Proof of Theorem opthprc

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2098	. . . . 5 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> ( <.x , (/) >. e. ((A X. { (/) }) u. (B X. { { (/) } })) <-> <.x , (/) >. e. (( C X. { (/) }) u. ( D X. { { (/) } }))))
2		0ex 3875	. . . . . . . . 9 |- (/) e. _V
3	2	snid 3394	. . . . . . . 8 |- (/) e. { (/) }
4		opelxp 4317	. . . . . . . 8 |- ( <.x , (/) >. e. (A X. { (/) }) <-> (x e. A /\ (/) e. { (/) }))
5	3, 4	mpbiran2 847	. . . . . . 7 |- ( <.x , (/) >. e. (A X. { (/) }) <-> x e. A)
6		opelxp 4317	. . . . . . . 8 |- ( <.x , (/) >. e. (B X. { { (/) } }) <-> (x e. B /\ (/) e. { { (/) } }))
7		0nep0 3909	. . . . . . . . . 10 |- (/) =/= { (/) }
8	2	elsnc 3390	. . . . . . . . . 10 |- ( (/) e. { { (/) } } <-> (/) = { (/) })
9	7, 8	nemtbir 2288	. . . . . . . . 9 |- -. (/) e. { { (/) } }
10	9	bianfi 853	. . . . . . . 8 |- ( (/) e. { { (/) } } <-> (x e. B /\ (/) e. { { (/) } }))
11	6, 10	bitr4i 176	. . . . . . 7 |- ( <.x , (/) >. e. (B X. { { (/) } }) <-> (/) e. { { (/) } })
12	5, 11	orbi12i 680	. . . . . 6 |- (( <.x , (/) >. e. (A X. { (/) }) \/ <.x , (/) >. e. (B X. { { (/) } })) <-> (x e. A \/ (/) e. { { (/) } }))
13		elun 3078	. . . . . 6 |- ( <.x , (/) >. e. ((A X. { (/) }) u. (B X. { { (/) } })) <-> ( <.x , (/) >. e. (A X. { (/) }) \/ <.x , (/) >. e. (B X. { { (/) } })))
14	9	biorfi 664	. . . . . 6 |- (x e. A <-> (x e. A \/ (/) e. { { (/) } }))
15	12, 13, 14	3bitr4ri 202	. . . . 5 |- (x e. A <-> <.x , (/) >. e. ((A X. { (/) }) u. (B X. { { (/) } })))
16		opelxp 4317	. . . . . . . 8 |- ( <.x , (/) >. e. ( C X. { (/) }) <-> (x e. C /\ (/) e. { (/) }))
17	3, 16	mpbiran2 847	. . . . . . 7 |- ( <.x , (/) >. e. ( C X. { (/) }) <-> x e. C)
18		opelxp 4317	. . . . . . . 8 |- ( <.x , (/) >. e. ( D X. { { (/) } }) <-> (x e. D /\ (/) e. { { (/) } }))
19	9	bianfi 853	. . . . . . . 8 |- ( (/) e. { { (/) } } <-> (x e. D /\ (/) e. { { (/) } }))
20	18, 19	bitr4i 176	. . . . . . 7 |- ( <.x , (/) >. e. ( D X. { { (/) } }) <-> (/) e. { { (/) } })
21	17, 20	orbi12i 680	. . . . . 6 |- (( <.x , (/) >. e. ( C X. { (/) }) \/ <.x , (/) >. e. ( D X. { { (/) } })) <-> (x e. C \/ (/) e. { { (/) } }))
22		elun 3078	. . . . . 6 |- ( <.x , (/) >. e. (( C X. { (/) }) u. ( D X. { { (/) } })) <-> ( <.x , (/) >. e. ( C X. { (/) }) \/ <.x , (/) >. e. ( D X. { { (/) } })))
23	9	biorfi 664	. . . . . 6 |- (x e. C <-> (x e. C \/ (/) e. { { (/) } }))
24	21, 22, 23	3bitr4ri 202	. . . . 5 |- (x e. C <-> <.x , (/) >. e. (( C X. { (/) }) u. ( D X. { { (/) } })))
25	1, 15, 24	3bitr4g 212	. . . 4 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> (x e. A <-> x e. C))
26	25	eqrdv 2035	. . 3 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> A = C)
27		eleq2 2098	. . . . 5 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> ( <.x , { (/) } >. e. ((A X. { (/) }) u. (B X. { { (/) } })) <-> <.x , { (/) } >. e. (( C X. { (/) }) u. ( D X. { { (/) } }))))
28		opelxp 4317	. . . . . . . 8 |- ( <.x , { (/) } >. e. (A X. { (/) }) <-> (x e. A /\ { (/) } e. { (/) }))
29		p0ex 3930	. . . . . . . . . . . 12 |- { (/) } e. _V
30	29	elsnc 3390	. . . . . . . . . . 11 |- ( { (/) } e. { (/) } <-> { (/) } = (/))
31		eqcom 2039	. . . . . . . . . . 11 |- ( { (/) } = (/) <-> (/) = { (/) })
32	30, 31	bitri 173	. . . . . . . . . 10 |- ( { (/) } e. { (/) } <-> (/) = { (/) })
33	7, 32	nemtbir 2288	. . . . . . . . 9 |- -. { (/) } e. { (/) }
34	33	bianfi 853	. . . . . . . 8 |- ( { (/) } e. { (/) } <-> (x e. A /\ { (/) } e. { (/) }))
35	28, 34	bitr4i 176	. . . . . . 7 |- ( <.x , { (/) } >. e. (A X. { (/) }) <-> { (/) } e. { (/) })
36	29	snid 3394	. . . . . . . 8 |- { (/) } e. { { (/) } }
37		opelxp 4317	. . . . . . . 8 |- ( <.x , { (/) } >. e. (B X. { { (/) } }) <-> (x e. B /\ { (/) } e. { { (/) } }))
38	36, 37	mpbiran2 847	. . . . . . 7 |- ( <.x , { (/) } >. e. (B X. { { (/) } }) <-> x e. B)
39	35, 38	orbi12i 680	. . . . . 6 |- (( <.x , { (/) } >. e. (A X. { (/) }) \/ <.x , { (/) } >. e. (B X. { { (/) } })) <-> ( { (/) } e. { (/) } \/ x e. B))
40		elun 3078	. . . . . 6 |- ( <.x , { (/) } >. e. ((A X. { (/) }) u. (B X. { { (/) } })) <-> ( <.x , { (/) } >. e. (A X. { (/) }) \/ <.x , { (/) } >. e. (B X. { { (/) } })))
41		biorf 662	. . . . . . 7 |- (-. { (/) } e. { (/) } -> (x e. B <-> ( { (/) } e. { (/) } \/ x e. B)))
42	33, 41	ax-mp 7	. . . . . 6 |- (x e. B <-> ( { (/) } e. { (/) } \/ x e. B))
43	39, 40, 42	3bitr4ri 202	. . . . 5 |- (x e. B <-> <.x , { (/) } >. e. ((A X. { (/) }) u. (B X. { { (/) } })))
44		opelxp 4317	. . . . . . . 8 |- ( <.x , { (/) } >. e. ( C X. { (/) }) <-> (x e. C /\ { (/) } e. { (/) }))
45	33	bianfi 853	. . . . . . . 8 |- ( { (/) } e. { (/) } <-> (x e. C /\ { (/) } e. { (/) }))
46	44, 45	bitr4i 176	. . . . . . 7 |- ( <.x , { (/) } >. e. ( C X. { (/) }) <-> { (/) } e. { (/) })
47		opelxp 4317	. . . . . . . 8 |- ( <.x , { (/) } >. e. ( D X. { { (/) } }) <-> (x e. D /\ { (/) } e. { { (/) } }))
48	36, 47	mpbiran2 847	. . . . . . 7 |- ( <.x , { (/) } >. e. ( D X. { { (/) } }) <-> x e. D)
49	46, 48	orbi12i 680	. . . . . 6 |- (( <.x , { (/) } >. e. ( C X. { (/) }) \/ <.x , { (/) } >. e. ( D X. { { (/) } })) <-> ( { (/) } e. { (/) } \/ x e. D))
50		elun 3078	. . . . . 6 |- ( <.x , { (/) } >. e. (( C X. { (/) }) u. ( D X. { { (/) } })) <-> ( <.x , { (/) } >. e. ( C X. { (/) }) \/ <.x , { (/) } >. e. ( D X. { { (/) } })))
51		biorf 662	. . . . . . 7 |- (-. { (/) } e. { (/) } -> (x e. D <-> ( { (/) } e. { (/) } \/ x e. D)))
52	33, 51	ax-mp 7	. . . . . 6 |- (x e. D <-> ( { (/) } e. { (/) } \/ x e. D))
53	49, 50, 52	3bitr4ri 202	. . . . 5 |- (x e. D <-> <.x , { (/) } >. e. (( C X. { (/) }) u. ( D X. { { (/) } })))
54	27, 43, 53	3bitr4g 212	. . . 4 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> (x e. B <-> x e. D))
55	54	eqrdv 2035	. . 3 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> B = D)
56	26, 55	jca 290	. 2 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) -> (A = C /\ B = D))
57		xpeq1 4302	. . 3 |- (A = C -> (A X. { (/) }) = ( C X. { (/) }))
58		xpeq1 4302	. . 3 |- (B = D -> (B X. { { (/) } }) = ( D X. { { (/) } }))
59		uneq12 3086	. . 3 |- (((A X. { (/) }) = ( C X. { (/) }) /\ (B X. { { (/) } }) = ( D X. { { (/) } })) -> ((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })))
60	57, 58, 59	syl2an 273	. 2 |- ((A = C /\ B = D) -> ((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })))
61	56, 60	impbii 117	1 |- (((A X. { (/) }) u. (B X. { { (/) } })) = (( C X. { (/) }) u. ( D X. { { (/) } })) <-> (A = C /\ B = D))

Syntax hints:  -. wn 3   /\ wa 97   <-> wb 98   \/ wo 628   = wceq 1242   e. wcel 1390   u. cun 2909   (/)c0 3218   {csn 3367   <.cop 3370   X. cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294

This theorem is referenced by: (None)