br8

Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013) (Revised by Mario Carneiro, 3-May-2015)

	Ref	Expression
Hypotheses	br8.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
	br8.2	$⊢ b = B \to (ψ \leftrightarrow χ)$
	br8.3	$⊢ c = C \to (χ \leftrightarrow θ)$
	br8.4	$⊢ d = D \to (θ \leftrightarrow τ)$
	br8.5	$⊢ e = E \to (τ \leftrightarrow η)$
	br8.6	$⊢ f = F \to (η \leftrightarrow ζ)$
	br8.7	$⊢ g = G \to (ζ \leftrightarrow σ)$
	br8.8	$⊢ h = H \to (σ \leftrightarrow ρ)$
	br8.9	$⊢ x = X \to P = Q$
	br8.10	$⊢ R = \{⟨p, q⟩ \| \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)\}$
Assertion	br8	$⊢ ((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ρ)$

Proof

Step	Hyp	Ref	Expression
1		br8.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
2		br8.2	$⊢ b = B \to (ψ \leftrightarrow χ)$
3		br8.3	$⊢ c = C \to (χ \leftrightarrow θ)$
4		br8.4	$⊢ d = D \to (θ \leftrightarrow τ)$
5		br8.5	$⊢ e = E \to (τ \leftrightarrow η)$
6		br8.6	$⊢ f = F \to (η \leftrightarrow ζ)$
7		br8.7	$⊢ g = G \to (ζ \leftrightarrow σ)$
8		br8.8	$⊢ h = H \to (σ \leftrightarrow ρ)$
9		br8.9	$⊢ x = X \to P = Q$
10		br8.10	$⊢ R = \{⟨p, q⟩ \| \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)\}$
11		opex	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ \in V$
12		opex	$⊢ ⟨⟨E, F⟩, ⟨G, H⟩⟩ \in V$
13		eqeq1	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩)$
14	13	3anbi1d	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to ((p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
15	14	rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
16	15	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
17	16	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
18	17	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
19	18	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
20		eqeq1	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩)$
21	20	3anbi2d	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
22	21	rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
23	22	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
24	23	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
25	24	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
26	25	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
27	11 12 19 26 10	brab	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)$
28		opex	$⊢ ⟨a, b⟩ \in V$
29		opex	$⊢ ⟨c, d⟩ \in V$
30	28 29	opth	$⊢ ⟨⟨a, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \leftrightarrow (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩)$
31		vex	$⊢ a \in V$
32		vex	$⊢ b \in V$
33	31 32	opth	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \leftrightarrow (a = A \land b = B)$
34	1 2	sylan9bb	$⊢ (a = A \land b = B) \to (φ \leftrightarrow χ)$
35	33 34	sylbi	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \to (φ \leftrightarrow χ)$
36		vex	$⊢ c \in V$
37		vex	$⊢ d \in V$
38	36 37	opth	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \leftrightarrow (c = C \land d = D)$
39	3 4	sylan9bb	$⊢ (c = C \land d = D) \to (χ \leftrightarrow τ)$
40	38 39	sylbi	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \to (χ \leftrightarrow τ)$
41	35 40	sylan9bb	$⊢ (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩) \to (φ \leftrightarrow τ)$
42	30 41	sylbi	$⊢ ⟨⟨a, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (φ \leftrightarrow τ)$
43	42	eqcoms	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \to (φ \leftrightarrow τ)$
44		opex	$⊢ ⟨e, f⟩ \in V$
45		opex	$⊢ ⟨g, h⟩ \in V$
46	44 45	opth	$⊢ ⟨⟨e, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (⟨e, f⟩ = ⟨E, F⟩ \land ⟨g, h⟩ = ⟨G, H⟩)$
47		vex	$⊢ e \in V$
48		vex	$⊢ f \in V$
49	47 48	opth	$⊢ ⟨e, f⟩ = ⟨E, F⟩ \leftrightarrow (e = E \land f = F)$
50	5 6	sylan9bb	$⊢ (e = E \land f = F) \to (τ \leftrightarrow ζ)$
51	49 50	sylbi	$⊢ ⟨e, f⟩ = ⟨E, F⟩ \to (τ \leftrightarrow ζ)$
52		vex	$⊢ g \in V$
53		vex	$⊢ h \in V$
54	52 53	opth	$⊢ ⟨g, h⟩ = ⟨G, H⟩ \leftrightarrow (g = G \land h = H)$
55	7 8	sylan9bb	$⊢ (g = G \land h = H) \to (ζ \leftrightarrow ρ)$
56	54 55	sylbi	$⊢ ⟨g, h⟩ = ⟨G, H⟩ \to (ζ \leftrightarrow ρ)$
57	51 56	sylan9bb	$⊢ (⟨e, f⟩ = ⟨E, F⟩ \land ⟨g, h⟩ = ⟨G, H⟩) \to (τ \leftrightarrow ρ)$
58	46 57	sylbi	$⊢ ⟨⟨e, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (τ \leftrightarrow ρ)$
59	58	eqcoms	$⊢ ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \to (τ \leftrightarrow ρ)$
60	43 59	sylan9bb	$⊢ (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩) \to (φ \leftrightarrow ρ)$
61	60	biimp3a	$⊢ (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ$
62	61	a1i	$⊢ (((((((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land (x \in S \land a \in P)) \land (b \in P \land c \in P)) \land (d \in P \land e \in P)) \land (f \in P \land g \in P)) \land h \in P) \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ)$
63	62	rexlimdva	$⊢ ((((((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land (x \in S \land a \in P)) \land (b \in P \land c \in P)) \land (d \in P \land e \in P)) \land (f \in P \land g \in P)) \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ)$
64	63	rexlimdvva	$⊢ (((((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land (x \in S \land a \in P)) \land (b \in P \land c \in P)) \land (d \in P \land e \in P)) \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ)$
65	64	rexlimdvva	$⊢ ((((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land (x \in S \land a \in P)) \land (b \in P \land c \in P)) \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ)$
66	65	rexlimdvva	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land (x \in S \land a \in P)) \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ)$
67	66	rexlimdvva	$⊢ ((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \to ρ)$
68		simpl11	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to X \in S$
69		simpl12	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to A \in Q$
70		simpl13	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to B \in Q$
71		simpl21	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to C \in Q$
72		simpl22	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to D \in Q$
73		simpl23	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to E \in Q$
74		simpl31	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to F \in Q$
75		simpl32	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to G \in Q$
76		simpl33	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to H \in Q$
77		eqidd	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩$
78		eqidd	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩$
79		simpr	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to ρ$
80		opeq1	$⊢ g = G \to ⟨g, h⟩ = ⟨G, h⟩$
81	80	opeq2d	$⊢ g = G \to ⟨⟨E, F⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩$
82	81	eqeq2d	$⊢ g = G \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩)$
83	82 7	3anbi23d	$⊢ g = G \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land ζ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩ \land σ))$
84		opeq2	$⊢ h = H \to ⟨G, h⟩ = ⟨G, H⟩$
85	84	opeq2d	$⊢ h = H \to ⟨⟨E, F⟩, ⟨G, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩$
86	85	eqeq2d	$⊢ h = H \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩)$
87	86 8	3anbi23d	$⊢ h = H \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩ \land σ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land ρ))$
88	83 87	rspc2ev	$⊢ (G \in Q \land H \in Q \land (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land ρ)) \to \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land ζ)$
89	75 76 77 78 79 88	syl113anc	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land ζ)$
90		opeq2	$⊢ d = D \to ⟨C, d⟩ = ⟨C, D⟩$
91	90	opeq2d	$⊢ d = D \to ⟨⟨A, B⟩, ⟨C, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩$
92	91	eqeq2d	$⊢ d = D \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩)$
93	92 4	3anbi13d	$⊢ d = D \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ))$
94	93	2rexbidv	$⊢ d = D \to (\exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ) \leftrightarrow \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ))$
95		opeq1	$⊢ e = E \to ⟨e, f⟩ = ⟨E, f⟩$
96	95	opeq1d	$⊢ e = E \to ⟨⟨e, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩$
97	96	eqeq2d	$⊢ e = E \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩)$
98	97 5	3anbi23d	$⊢ e = E \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land η))$
99	98	2rexbidv	$⊢ e = E \to (\exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ) \leftrightarrow \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land η))$
100		opeq2	$⊢ f = F \to ⟨E, f⟩ = ⟨E, F⟩$
101	100	opeq1d	$⊢ f = F \to ⟨⟨E, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩$
102	101	eqeq2d	$⊢ f = F \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩)$
103	102 6	3anbi23d	$⊢ f = F \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land η) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land ζ))$
104	103	2rexbidv	$⊢ f = F \to (\exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land η) \leftrightarrow \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land ζ))$
105	94 99 104	rspc3ev	$⊢ ((D \in Q \land E \in Q \land F \in Q) \land \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land ζ)) \to \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ)$
106	72 73 74 89 105	syl31anc	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ)$
107		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
108	107	opeq1d	$⊢ a = A \to ⟨⟨a, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩$
109	108	eqeq2d	$⊢ a = A \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩)$
110	109 1	3anbi13d	$⊢ a = A \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
111	110	rexbidv	$⊢ a = A \to (\exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
112	111	2rexbidv	$⊢ a = A \to (\exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
113	112	2rexbidv	$⊢ a = A \to (\exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
114		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
115	114	opeq1d	$⊢ b = B \to ⟨⟨A, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩$
116	115	eqeq2d	$⊢ b = B \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩)$
117	116 2	3anbi13d	$⊢ b = B \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
118	117	rexbidv	$⊢ b = B \to (\exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
119	118	2rexbidv	$⊢ b = B \to (\exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
120	119	2rexbidv	$⊢ b = B \to (\exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
121		opeq1	$⊢ c = C \to ⟨c, d⟩ = ⟨C, d⟩$
122	121	opeq2d	$⊢ c = C \to ⟨⟨A, B⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩$
123	122	eqeq2d	$⊢ c = C \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩)$
124	123 3	3anbi13d	$⊢ c = C \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
125	124	rexbidv	$⊢ c = C \to (\exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
126	125	2rexbidv	$⊢ c = C \to (\exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
127	126	2rexbidv	$⊢ c = C \to (\exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
128	113 120 127	rspc3ev	$⊢ ((A \in Q \land B \in Q \land C \in Q) \land \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ)) \to \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)$
129	69 70 71 106 128	syl31anc	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)$
130	9	rexeqdv	$⊢ x = X \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
131	9 130	rexeqbidv	$⊢ x = X \to (\exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
132	9 131	rexeqbidv	$⊢ x = X \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
133	9 132	rexeqbidv	$⊢ x = X \to (\exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
134	9 133	rexeqbidv	$⊢ x = X \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
135	9 134	rexeqbidv	$⊢ x = X \to (\exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
136	9 135	rexeqbidv	$⊢ x = X \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists b \in Q \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
137	9 136	rexeqbidv	$⊢ x = X \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
138	137	rspcev	$⊢ (X \in S \land \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q \exists g \in Q \exists h \in Q (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)) \to \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)$
139	68 129 138	syl2anc	$⊢ (((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \land ρ) \to \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ)$
140	139	ex	$⊢ ((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \to (ρ \to \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ))$
141	67 140	impbid	$⊢ ((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land φ) \leftrightarrow ρ)$
142	27 141	bitrid	$⊢ ((X \in S \land A \in Q \land B \in Q) \land (C \in Q \land D \in Q \land E \in Q) \land (F \in Q \land G \in Q \land H \in Q)) \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ρ)$

Metamath Proof Explorer

Theorem br8

Proof