Theorem th3qlem1 3250

Description: Lemma for Exercise 44 version of Theorem 3Q of [Enderton] p. 60. The third hypothesis is the compatibility assumption.

Hypotheses

Ref	Expression
th3qlem1.1	⊢ Er R
th3qlem1.2	⊢ dom R = S
th3qlem1.3	⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → ((yRw ∧ zRv) → (yFz)R(wFv)))

Assertion

Ref	Expression
th3qlem1	⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ∃*x∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R))

Distinct variable group(s):   x,y,z,w,v,F   x,R,y,z,w,v   x,S,y,z,w,v   x,A,y,z,w,v   x,B,y,z,w,v

Proof of Theorem th3qlem1

Step	Hyp	Ref	Expression
1		an4 388	. . . . . . . . . . . . 13 ⊢ (((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R)) ↔ ((A = [y]R ∧ A = [w]R) ∧ (B = [z]R ∧ B = [v]R)))
2	1	anbi2i 367	. . . . . . . . . . . 12 ⊢ ((((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (B ∈ (S / R) ∧ B ∈ (S / R))) ∧ ((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R))) ↔ (((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (B ∈ (S / R) ∧ B ∈ (S / R))) ∧ ((A = [y]R ∧ A = [w]R) ∧ (B = [z]R ∧ B = [v]R))))
3		an4 388	. . . . . . . . . . . 12 ⊢ ((((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (B ∈ (S / R) ∧ B ∈ (S / R))) ∧ ((A = [y]R ∧ A = [w]R) ∧ (B = [z]R ∧ B = [v]R))) ↔ (((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (A = [y]R ∧ A = [w]R)) ∧ ((B ∈ (S / R) ∧ B ∈ (S / R)) ∧ (B = [z]R ∧ B = [v]R))))
4		an4 388	. . . . . . . . . . . . . 14 ⊢ (((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (A = [y]R ∧ A = [w]R)) ↔ ((A ∈ (S / R) ∧ A = [y]R) ∧ (A ∈ (S / R) ∧ A = [w]R)))
5		eleq1 1149	. . . . . . . . . . . . . . . 16 ⊢ (A = [y]R → (A ∈ (S / R) ↔ [y]R ∈ (S / R)))
6	5	pm5.32ri 490	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ (S / R) ∧ A = [y]R) ↔ ([y]R ∈ (S / R) ∧ A = [y]R))
7		eleq1 1149	. . . . . . . . . . . . . . . 16 ⊢ (A = [w]R → (A ∈ (S / R) ↔ [w]R ∈ (S / R)))
8	7	pm5.32ri 490	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ (S / R) ∧ A = [w]R) ↔ ([w]R ∈ (S / R) ∧ A = [w]R))
9	6, 8	anbi12i 369	. . . . . . . . . . . . . 14 ⊢ (((A ∈ (S / R) ∧ A = [y]R) ∧ (A ∈ (S / R) ∧ A = [w]R)) ↔ (([y]R ∈ (S / R) ∧ A = [y]R) ∧ ([w]R ∈ (S / R) ∧ A = [w]R)))
10	4, 9	bitr 151	. . . . . . . . . . . . 13 ⊢ (((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (A = [y]R ∧ A = [w]R)) ↔ (([y]R ∈ (S / R) ∧ A = [y]R) ∧ ([w]R ∈ (S / R) ∧ A = [w]R)))
11		an4 388	. . . . . . . . . . . . . 14 ⊢ (((B ∈ (S / R) ∧ B ∈ (S / R)) ∧ (B = [z]R ∧ B = [v]R)) ↔ ((B ∈ (S / R) ∧ B = [z]R) ∧ (B ∈ (S / R) ∧ B = [v]R)))
12		eleq1 1149	. . . . . . . . . . . . . . . 16 ⊢ (B = [z]R → (B ∈ (S / R) ↔ [z]R ∈ (S / R)))
13	12	pm5.32ri 490	. . . . . . . . . . . . . . 15 ⊢ ((B ∈ (S / R) ∧ B = [z]R) ↔ ([z]R ∈ (S / R) ∧ B = [z]R))
14		eleq1 1149	. . . . . . . . . . . . . . . 16 ⊢ (B = [v]R → (B ∈ (S / R) ↔ [v]R ∈ (S / R)))
15	14	pm5.32ri 490	. . . . . . . . . . . . . . 15 ⊢ ((B ∈ (S / R) ∧ B = [v]R) ↔ ([v]R ∈ (S / R) ∧ B = [v]R))
16	13, 15	anbi12i 369	. . . . . . . . . . . . . 14 ⊢ (((B ∈ (S / R) ∧ B = [z]R) ∧ (B ∈ (S / R) ∧ B = [v]R)) ↔ (([z]R ∈ (S / R) ∧ B = [z]R) ∧ ([v]R ∈ (S / R) ∧ B = [v]R)))
17	11, 16	bitr 151	. . . . . . . . . . . . 13 ⊢ (((B ∈ (S / R) ∧ B ∈ (S / R)) ∧ (B = [z]R ∧ B = [v]R)) ↔ (([z]R ∈ (S / R) ∧ B = [z]R) ∧ ([v]R ∈ (S / R) ∧ B = [v]R)))
18	10, 17	anbi12i 369	. . . . . . . . . . . 12 ⊢ ((((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (A = [y]R ∧ A = [w]R)) ∧ ((B ∈ (S / R) ∧ B ∈ (S / R)) ∧ (B = [z]R ∧ B = [v]R))) ↔ ((([y]R ∈ (S / R) ∧ A = [y]R) ∧ ([w]R ∈ (S / R) ∧ A = [w]R)) ∧ (([z]R ∈ (S / R) ∧ B = [z]R) ∧ ([v]R ∈ (S / R) ∧ B = [v]R))))
19	2, 3, 18	3bitr 155	. . . . . . . . . . 11 ⊢ ((((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (B ∈ (S / R) ∧ B ∈ (S / R))) ∧ ((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R))) ↔ ((([y]R ∈ (S / R) ∧ A = [y]R) ∧ ([w]R ∈ (S / R) ∧ A = [w]R)) ∧ (([z]R ∈ (S / R) ∧ B = [z]R) ∧ ([v]R ∈ (S / R) ∧ B = [v]R))))
20		pm3.26 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((y ∈ S ∧ w ∈ S) → y ∈ S)
21		th3qlem1.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom R = S
22	21	eleq2i 1153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (y ∈ dom R ↔ y ∈ S)
23	20, 22	sylibr 175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ S ∧ w ∈ S) → y ∈ dom R)
24		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ w ∈ V
25		th3qlem1.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Er R
26	24, 25	erthdm 3220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ dom R → ([y]R = [w]R ↔ yRw))
27	23, 26	syl 12	. . . . . . . . . . . . . . . . . . 19 ⊢ ((y ∈ S ∧ w ∈ S) → ([y]R = [w]R ↔ yRw))
28		pm3.26 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((z ∈ S ∧ v ∈ S) → z ∈ S)
29	21	eleq2i 1153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (z ∈ dom R ↔ z ∈ S)
30	28, 29	sylibr 175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((z ∈ S ∧ v ∈ S) → z ∈ dom R)
31		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ v ∈ V
32	31, 25	erthdm 3220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (z ∈ dom R → ([z]R = [v]R ↔ zRv))
33	30, 32	syl 12	. . . . . . . . . . . . . . . . . . 19 ⊢ ((z ∈ S ∧ v ∈ S) → ([z]R = [v]R ↔ zRv))
34	27, 33	bi2anan9 478	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → (([y]R = [w]R ∧ [z]R = [v]R) ↔ (yRw ∧ zRv)))
35		th3qlem1.3	. . . . . . . . . . . . . . . . . 18 ⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → ((yRw ∧ zRv) → (yFz)R(wFv)))
36	34, 35	sylbid 178	. . . . . . . . . . . . . . . . 17 ⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → (([y]R = [w]R ∧ [z]R = [v]R) → (yFz)R(wFv)))
37		cleq12 1113	. . . . . . . . . . . . . . . . . 18 ⊢ ((x = [(yFz)]R ∧ u = [(wFv)]R) → (x = u ↔ [(yFz)]R = [(wFv)]R))
38		oprex 3018	. . . . . . . . . . . . . . . . . . 19 ⊢ (yFz) ∈ V
39		oprex 3018	. . . . . . . . . . . . . . . . . . 19 ⊢ (wFv) ∈ V
40	38, 39, 25	erthi 3218	. . . . . . . . . . . . . . . . . 18 ⊢ ((yFz)R(wFv) → [(yFz)]R = [(wFv)]R)
41	37, 40	syl5bir 184	. . . . . . . . . . . . . . . . 17 ⊢ ((x = [(yFz)]R ∧ u = [(wFv)]R) → ((yFz)R(wFv) → x = u))
42	36, 41	syl9 55	. . . . . . . . . . . . . . . 16 ⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → (([y]R = [w]R ∧ [z]R = [v]R) → x = u)))
43	42	com23 32	. . . . . . . . . . . . . . 15 ⊢ (((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) → (([y]R = [w]R ∧ [z]R = [v]R) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u)))
44	43	imp 277	. . . . . . . . . . . . . 14 ⊢ ((((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)) ∧ ([y]R = [w]R ∧ [z]R = [v]R)) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u))
45		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ y ∈ V
46	45, 25, 21	ecelqsdm 3235	. . . . . . . . . . . . . . . 16 ⊢ ([y]R ∈ (S / R) → y ∈ S)
47	24, 25, 21	ecelqsdm 3235	. . . . . . . . . . . . . . . 16 ⊢ ([w]R ∈ (S / R) → w ∈ S)
48	46, 47	anim12i 268	. . . . . . . . . . . . . . 15 ⊢ (([y]R ∈ (S / R) ∧ [w]R ∈ (S / R)) → (y ∈ S ∧ w ∈ S))
49		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ z ∈ V
50	49, 25, 21	ecelqsdm 3235	. . . . . . . . . . . . . . . 16 ⊢ ([z]R ∈ (S / R) → z ∈ S)
51	31, 25, 21	ecelqsdm 3235	. . . . . . . . . . . . . . . 16 ⊢ ([v]R ∈ (S / R) → v ∈ S)
52	50, 51	anim12i 268	. . . . . . . . . . . . . . 15 ⊢ (([z]R ∈ (S / R) ∧ [v]R ∈ (S / R)) → (z ∈ S ∧ v ∈ S))
53	48, 52	anim12i 268	. . . . . . . . . . . . . 14 ⊢ ((([y]R ∈ (S / R) ∧ [w]R ∈ (S / R)) ∧ ([z]R ∈ (S / R) ∧ [v]R ∈ (S / R))) → ((y ∈ S ∧ w ∈ S) ∧ (z ∈ S ∧ v ∈ S)))
54		cleq1 1107	. . . . . . . . . . . . . . . 16 ⊢ (A = [y]R → (A = [w]R ↔ [y]R = [w]R))
55	54	biimpa 324	. . . . . . . . . . . . . . 15 ⊢ ((A = [y]R ∧ A = [w]R) → [y]R = [w]R)
56		cleq1 1107	. . . . . . . . . . . . . . . 16 ⊢ (B = [z]R → (B = [v]R ↔ [z]R = [v]R))
57	56	biimpa 324	. . . . . . . . . . . . . . 15 ⊢ ((B = [z]R ∧ B = [v]R) → [z]R = [v]R)
58	55, 57	anim12i 268	. . . . . . . . . . . . . 14 ⊢ (((A = [y]R ∧ A = [w]R) ∧ (B = [z]R ∧ B = [v]R)) → ([y]R = [w]R ∧ [z]R = [v]R))
59	44, 53, 58	syl2an 349	. . . . . . . . . . . . 13 ⊢ (((([y]R ∈ (S / R) ∧ [w]R ∈ (S / R)) ∧ ([z]R ∈ (S / R) ∧ [v]R ∈ (S / R))) ∧ ((A = [y]R ∧ A = [w]R) ∧ (B = [z]R ∧ B = [v]R))) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u))
60	59	an4s 390	. . . . . . . . . . . 12 ⊢ (((([y]R ∈ (S / R) ∧ [w]R ∈ (S / R)) ∧ (A = [y]R ∧ A = [w]R)) ∧ (([z]R ∈ (S / R) ∧ [v]R ∈ (S / R)) ∧ (B = [z]R ∧ B = [v]R))) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u))
61		an4 388	. . . . . . . . . . . 12 ⊢ ((([y]R ∈ (S / R) ∧ A = [y]R) ∧ ([w]R ∈ (S / R) ∧ A = [w]R)) ↔ (([y]R ∈ (S / R) ∧ [w]R ∈ (S / R)) ∧ (A = [y]R ∧ A = [w]R)))
62		an4 388	. . . . . . . . . . . 12 ⊢ ((([z]R ∈ (S / R) ∧ B = [z]R) ∧ ([v]R ∈ (S / R) ∧ B = [v]R)) ↔ (([z]R ∈ (S / R) ∧ [v]R ∈ (S / R)) ∧ (B = [z]R ∧ B = [v]R)))
63	60, 61, 62	syl2anb 350	. . . . . . . . . . 11 ⊢ (((([y]R ∈ (S / R) ∧ A = [y]R) ∧ ([w]R ∈ (S / R) ∧ A = [w]R)) ∧ (([z]R ∈ (S / R) ∧ B = [z]R) ∧ ([v]R ∈ (S / R) ∧ B = [v]R))) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u))
64	19, 63	sylbi 174	. . . . . . . . . 10 ⊢ ((((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (B ∈ (S / R) ∧ B ∈ (S / R))) ∧ ((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R))) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u))
65		anidm 331	. . . . . . . . . . 11 ⊢ ((A ∈ (S / R) ∧ A ∈ (S / R)) ↔ A ∈ (S / R))
66		anidm 331	. . . . . . . . . . 11 ⊢ ((B ∈ (S / R) ∧ B ∈ (S / R)) ↔ B ∈ (S / R))
67	65, 66	anbi12i 369	. . . . . . . . . 10 ⊢ (((A ∈ (S / R) ∧ A ∈ (S / R)) ∧ (B ∈ (S / R) ∧ B ∈ (S / R))) ↔ (A ∈ (S / R) ∧ B ∈ (S / R)))
68	64, 67	sylanbr 345	. . . . . . . . 9 ⊢ (((A ∈ (S / R) ∧ B ∈ (S / R)) ∧ ((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R))) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u))
69	68	exp 291	. . . . . . . 8 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → (((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R)) → ((x = [(yFz)]R ∧ u = [(wFv)]R) → x = u)))
70	69	imp3a 279	. . . . . . 7 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ((((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R)) ∧ (x = [(yFz)]R ∧ u = [(wFv)]R)) → x = u))
71		an4 388	. . . . . . 7 ⊢ ((((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) ↔ (((A = [y]R ∧ B = [z]R) ∧ (A = [w]R ∧ B = [v]R)) ∧ (x = [(yFz)]R ∧ u = [(wFv)]R)))
72	70, 71	syl5ib 181	. . . . . 6 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ((((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) → x = u))
73	72	19.23advv 955	. . . . 5 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → (∃w∃v(((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) → x = u))
74	73	19.23advv 955	. . . 4 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → (∃y∃z∃w∃v(((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) → x = u))
75		ee4anv 982	. . . 4 ⊢ (∃y∃z∃w∃v(((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) ↔ (∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ∃w∃v((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)))
76	74, 75	syl5ibr 182	. . 3 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ((∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ∃w∃v((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) → x = u))
77	76	19.21aivv 944	. 2 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ∀x∀u((∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ∃w∃v((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) → x = u))
78		cleq1 1107	. . . . . 6 ⊢ (x = u → (x = [(yFz)]R ↔ u = [(yFz)]R))
79	78	anbi2d 468	. . . . 5 ⊢ (x = u → (((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ↔ ((A = [y]R ∧ B = [z]R) ∧ u = [(yFz)]R)))
80	79	bi2exdv 938	. . . 4 ⊢ (x = u → (∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ↔ ∃y∃z((A = [y]R ∧ B = [z]R) ∧ u = [(yFz)]R)))
81		eceq2 3215	. . . . . . . 8 ⊢ (y = w → [y]R = [w]R)
82	81	cleq2d 1112	. . . . . . 7 ⊢ (y = w → (A = [y]R ↔ A = [w]R))
83		eceq2 3215	. . . . . . . 8 ⊢ (z = v → [z]R = [v]R)
84	83	cleq2d 1112	. . . . . . 7 ⊢ (z = v → (B = [z]R ↔ B = [v]R))
85	82, 84	bi2anan9 478	. . . . . 6 ⊢ ((y = w ∧ z = v) → ((A = [y]R ∧ B = [z]R) ↔ (A = [w]R ∧ B = [v]R)))
86		opreq12 3008	. . . . . . . 8 ⊢ ((y = w ∧ z = v) → (yFz) = (wFv))
87		eceq2 3215	. . . . . . . 8 ⊢ ((yFz) = (wFv) → [(yFz)]R = [(wFv)]R)
88	86, 87	syl 12	. . . . . . 7 ⊢ ((y = w ∧ z = v) → [(yFz)]R = [(wFv)]R)
89	88	cleq2d 1112	. . . . . 6 ⊢ ((y = w ∧ z = v) → (u = [(yFz)]R ↔ u = [(wFv)]R))
90	85, 89	anbi12d 476	. . . . 5 ⊢ ((y = w ∧ z = v) → (((A = [y]R ∧ B = [z]R) ∧ u = [(yFz)]R) ↔ ((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)))
91	90	cbvex2v 976	. . . 4 ⊢ (∃y∃z((A = [y]R ∧ B = [z]R) ∧ u = [(yFz)]R) ↔ ∃w∃v((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R))
92	80, 91	syl6bb 414	. . 3 ⊢ (x = u → (∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ↔ ∃w∃v((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)))
93	92	mo4 1029	. 2 ⊢ (∃*x∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ↔ ∀x∀u((∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R) ∧ ∃w∃v((A = [w]R ∧ B = [v]R) ∧ u = [(wFv)]R)) → x = u))
94	77, 93	sylibr 175	1 ⊢ ((A ∈ (S / R) ∧ B ∈ (S / R)) → ∃*x∃y∃z((A = [y]R ∧ B = [z]R) ∧ x = [(yFz)]R))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797  ∃*wmo 1008   = wceq 1091   ∈ wcel 1092   class class class wbr 2054  dom cdm 2410  (class class class)co 3001  Er wer 3197  [cec 3198   / cqs 3199

This theorem is referenced by:  th3qlem2 3251

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-xp 2424  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fv 2438  df-opr 3003  df-er 3200  df-ec 3202  df-qs 3205

metamath.org