br4 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > br4		Structured version Visualization version GIF version

Theorem br4 30901

Description: Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.)

**Hypotheses**
Ref	Expression
br4.1	⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
br4.2	⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
br4.3	⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
br4.4	⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
br4.5	⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
br4.6	⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}

**Assertion**
Ref	Expression
br4	⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))

Distinct variable groups: 𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥,𝐴 𝐵,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝜒,𝑏 𝑄,𝑎,𝑏,𝑐,𝑑,𝑥 𝐶,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝐷,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝜓,𝑎 𝑋,𝑎,𝑏,𝑐,𝑑,𝑥 𝑃,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞 𝑆,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝜏,𝑎,𝑏,𝑐,𝑑,𝑥 𝜃,𝑐 𝜑,𝑝,𝑞,𝑥 Allowed substitution hints: 𝜑(𝑎,𝑏,𝑐,𝑑) 𝜓(𝑥,𝑞,𝑝,𝑏,𝑐,𝑑) 𝜒(𝑥,𝑞,𝑝,𝑎,𝑐,𝑑) 𝜃(𝑥,𝑞,𝑝,𝑎,𝑏,𝑑) 𝜏(𝑞,𝑝) 𝑃(𝑥) 𝑄(𝑞,𝑝) 𝑅(𝑥,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝑋(𝑞,𝑝)

**Proof of Theorem br4**
Step	Hyp	Ref	Expression
1		opex 4859	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		opex 4859	. . 3 ⊢ ⟨𝐶, 𝐷⟩ ∈ V
3		eqeq1 2614	. . . . . . 7 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩))
4	3	3anbi1d 1395	. . . . . 6 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
5	4	rexbidv 3034	. . . . 5 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
6	5	2rexbidv 3039	. . . 4 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
7	6	2rexbidv 3039	. . 3 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
8		eqeq1 2614	. . . . . . 7 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (𝑞 = ⟨𝑐, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩))
9	8	3anbi2d 1396	. . . . . 6 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
10	9	rexbidv 3034	. . . . 5 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
11	10	2rexbidv 3039	. . . 4 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
12	11	2rexbidv 3039	. . 3 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
13		br4.6	. . 3 ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}
14	1, 2, 7, 12, 13	brab 4923	. 2 ⊢ (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
15		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
16		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
17	15, 16	opth 4871	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵))
18		br4.1	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
19		br4.2	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
20	18, 19	sylan9bb 732	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜒))
21	17, 20	sylbi 206	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ 𝜒))
22	21	eqcoms 2618	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))
23		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
24		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑑 ∈ V
25	23, 24	opth 4871	. . . . . . . . . . 11 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))
26		br4.3	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
27		br4.4	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
28	26, 27	sylan9bb 732	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜒 ↔ 𝜏))
29	25, 28	sylbi 206	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜒 ↔ 𝜏))
30	29	eqcoms 2618	. . . . . . . . 9 ⊢ (⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ → (𝜒 ↔ 𝜏))
31	22, 30	sylan9bb 732	. . . . . . . 8 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩) → (𝜑 ↔ 𝜏))
32	31	biimp3a 1424	. . . . . . 7 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏)
33	32	a1i 11	. . . . . 6 ⊢ (((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ 𝑑 ∈ 𝑃) → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
34	33	rexlimdva 3013	. . . . 5 ⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
35	34	rexlimdvva 3020	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
36	35	rexlimdvva 3020	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
37		simpl1 1057	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝑋 ∈ 𝑆)
38		simpl2l 1107	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐴 ∈ 𝑄)
39		simpl2r 1108	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐵 ∈ 𝑄)
40		simpl3l 1109	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐶 ∈ 𝑄)
41		simpl3r 1110	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐷 ∈ 𝑄)
42		eqidd 2611	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
43		eqidd 2611	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩)
44		simpr 476	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝜏)
45		opeq1 4340	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
46	45	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩))
47	46, 26	3anbi23d 1394	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ∧ 𝜃)))
48		opeq2 4341	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
49	48	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩))
50	49, 27	3anbi23d 1394	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ∧ 𝜃) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩ ∧ 𝜏)))
51	47, 50	rspc2ev 3295	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩ ∧ 𝜏)) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒))
52	40, 41, 42, 43, 44, 51	syl113anc 1330	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒))
53		opeq1 4340	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
54	53	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩))
55	54, 18	3anbi13d 1393	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓)))
56	55	2rexbidv 3039	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓)))
57		opeq2 4341	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
58	57	eqeq2d 2620	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
59	58, 19	3anbi13d 1393	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)))
60	59	2rexbidv 3039	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)))
61	56, 60	rspc2ev 3295	. . . . . 6 ⊢ ((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
62	38, 39, 52, 61	syl3anc 1318	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
63		br4.5	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
64	63	rexeqdv 3122	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
65	63, 64	rexeqbidv 3130	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
66	63, 65	rexeqbidv 3130	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
67	63, 66	rexeqbidv 3130	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
68	67	rspcev 3282	. . . . 5 ⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
69	37, 62, 68	syl2anc 691	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
70	69	ex 449	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (𝜏 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
71	36, 70	impbid 201	. 2 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ 𝜏))
72	14, 71	syl5bb 271	1 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∃wrex 2897 ⟨cop 4131 class class class wbr 4583 {copab 4642

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644

This theorem is referenced by: (None)

W3C validator