br6

Description: Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013) (Revised by Mario Carneiro, 3-May-2015)

	Ref	Expression
Hypotheses	br6.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
	br6.2	$⊢ b = B \to (ψ \leftrightarrow χ)$
	br6.3	$⊢ c = C \to (χ \leftrightarrow θ)$
	br6.4	$⊢ d = D \to (θ \leftrightarrow τ)$
	br6.5	$⊢ e = E \to (τ \leftrightarrow η)$
	br6.6	$⊢ f = F \to (η \leftrightarrow ζ)$
	br6.7	$⊢ x = X \to P = Q$
	br6.8	$⊢ 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 (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ)\}$
Assertion	br6	$⊢ (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)) \to (⟨A, ⟨B, C⟩⟩ R ⟨D, ⟨E, F⟩⟩ \leftrightarrow ζ)$

Proof

Step	Hyp	Ref	Expression
1		br6.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
2		br6.2	$⊢ b = B \to (ψ \leftrightarrow χ)$
3		br6.3	$⊢ c = C \to (χ \leftrightarrow θ)$
4		br6.4	$⊢ d = D \to (θ \leftrightarrow τ)$
5		br6.5	$⊢ e = E \to (τ \leftrightarrow η)$
6		br6.6	$⊢ f = F \to (η \leftrightarrow ζ)$
7		br6.7	$⊢ x = X \to P = Q$
8		br6.8	$⊢ 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 (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ)\}$
9		opex	$⊢ ⟨A, ⟨B, C⟩⟩ \in V$
10		opex	$⊢ ⟨D, ⟨E, F⟩⟩ \in V$
11		eqeq1	$⊢ p = ⟨A, ⟨B, C⟩⟩ \to (p = ⟨a, ⟨b, c⟩⟩ \leftrightarrow ⟨A, ⟨B, C⟩⟩ = ⟨a, ⟨b, c⟩⟩)$
12		eqcom	$⊢ ⟨A, ⟨B, C⟩⟩ = ⟨a, ⟨b, c⟩⟩ \leftrightarrow ⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩$
13	11 12	bitrdi	$⊢ p = ⟨A, ⟨B, C⟩⟩ \to (p = ⟨a, ⟨b, c⟩⟩ \leftrightarrow ⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩)$
14	13	3anbi1d	$⊢ p = ⟨A, ⟨B, C⟩⟩ \to ((p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ))$
15	14	rexbidv	$⊢ p = ⟨A, ⟨B, C⟩⟩ \to (\exists f \in P (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ))$
16	15	2rexbidv	$⊢ p = ⟨A, ⟨B, C⟩⟩ \to (\exists d \in P \exists e \in P \exists f \in P (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ))$
17	16	2rexbidv	$⊢ p = ⟨A, ⟨B, C⟩⟩ \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ))$
18	17	2rexbidv	$⊢ p = ⟨A, ⟨B, C⟩⟩ \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 (p = ⟨a, ⟨b, c⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ))$
19		eqeq1	$⊢ q = ⟨D, ⟨E, F⟩⟩ \to (q = ⟨d, ⟨e, f⟩⟩ \leftrightarrow ⟨D, ⟨E, F⟩⟩ = ⟨d, ⟨e, f⟩⟩)$
20		eqcom	$⊢ ⟨D, ⟨E, F⟩⟩ = ⟨d, ⟨e, f⟩⟩ \leftrightarrow ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩$
21	19 20	bitrdi	$⊢ q = ⟨D, ⟨E, F⟩⟩ \to (q = ⟨d, ⟨e, f⟩⟩ \leftrightarrow ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩)$
22	21	3anbi2d	$⊢ q = ⟨D, ⟨E, F⟩⟩ \to ((⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
23	22	rexbidv	$⊢ q = ⟨D, ⟨E, F⟩⟩ \to (\exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
24	23	2rexbidv	$⊢ q = ⟨D, ⟨E, F⟩⟩ \to (\exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
25	24	2rexbidv	$⊢ q = ⟨D, ⟨E, F⟩⟩ \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \land φ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
26	25	2rexbidv	$⊢ q = ⟨D, ⟨E, F⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land q = ⟨d, ⟨e, f⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
27	9 10 18 26 8	brab	$⊢ ⟨A, ⟨B, C⟩⟩ R ⟨D, ⟨E, F⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ)$
28		vex	$⊢ a \in V$
29		opex	$⊢ ⟨b, c⟩ \in V$
30	28 29	opth	$⊢ ⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \leftrightarrow (a = A \land ⟨b, c⟩ = ⟨B, C⟩)$
31		vex	$⊢ b \in V$
32		vex	$⊢ c \in V$
33	31 32	opth	$⊢ ⟨b, c⟩ = ⟨B, C⟩ \leftrightarrow (b = B \land c = C)$
34	2 3	sylan9bb	$⊢ (b = B \land c = C) \to (ψ \leftrightarrow θ)$
35	33 34	sylbi	$⊢ ⟨b, c⟩ = ⟨B, C⟩ \to (ψ \leftrightarrow θ)$
36	1 35	sylan9bb	$⊢ (a = A \land ⟨b, c⟩ = ⟨B, C⟩) \to (φ \leftrightarrow θ)$
37	30 36	sylbi	$⊢ ⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \to (φ \leftrightarrow θ)$
38		vex	$⊢ d \in V$
39		opex	$⊢ ⟨e, f⟩ \in V$
40	38 39	opth	$⊢ ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \leftrightarrow (d = D \land ⟨e, f⟩ = ⟨E, F⟩)$
41		vex	$⊢ e \in V$
42		vex	$⊢ f \in V$
43	41 42	opth	$⊢ ⟨e, f⟩ = ⟨E, F⟩ \leftrightarrow (e = E \land f = F)$
44	5 6	sylan9bb	$⊢ (e = E \land f = F) \to (τ \leftrightarrow ζ)$
45	43 44	sylbi	$⊢ ⟨e, f⟩ = ⟨E, F⟩ \to (τ \leftrightarrow ζ)$
46	4 45	sylan9bb	$⊢ (d = D \land ⟨e, f⟩ = ⟨E, F⟩) \to (θ \leftrightarrow ζ)$
47	40 46	sylbi	$⊢ ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \to (θ \leftrightarrow ζ)$
48	37 47	sylan9bb	$⊢ (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩) \to (φ \leftrightarrow ζ)$
49	48	biimp3a	$⊢ (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \to ζ$
50	49	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 (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) \to ((⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \to ζ)$
51	50	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 (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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \to ζ)$
52	51	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 (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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \to ζ)$
53	52	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 (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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \to ζ)$
54	53	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)) \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \to ζ)$
55		simpl1	$⊢ ((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 ζ) \to X \in S$
56		simpl2	$⊢ ((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 ζ) \to (A \in Q \land B \in Q \land C \in Q)$
57		opeq1	$⊢ d = D \to ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨e, f⟩⟩$
58	57	eqeq1d	$⊢ d = D \to (⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \leftrightarrow ⟨D, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩)$
59	58 4	3anbi23d	$⊢ d = D \to ((⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land θ) \leftrightarrow (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land τ))$
60		opeq1	$⊢ e = E \to ⟨e, f⟩ = ⟨E, f⟩$
61	60	opeq2d	$⊢ e = E \to ⟨D, ⟨e, f⟩⟩ = ⟨D, ⟨E, f⟩⟩$
62	61	eqeq1d	$⊢ e = E \to (⟨D, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \leftrightarrow ⟨D, ⟨E, f⟩⟩ = ⟨D, ⟨E, F⟩⟩)$
63	62 5	3anbi23d	$⊢ e = E \to ((⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land τ) \leftrightarrow (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land η))$
64		opeq2	$⊢ f = F \to ⟨E, f⟩ = ⟨E, F⟩$
65	64	opeq2d	$⊢ f = F \to ⟨D, ⟨E, f⟩⟩ = ⟨D, ⟨E, F⟩⟩$
66	65	eqeq1d	$⊢ f = F \to (⟨D, ⟨E, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \leftrightarrow ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩)$
67	66 6	3anbi23d	$⊢ f = F \to ((⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land η) \leftrightarrow (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ζ))$
68		eqid	$⊢ ⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩$
69		eqid	$⊢ ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩$
70	68 69	pm3.2i	$⊢ (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩)$
71		df-3an	$⊢ (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ζ) \leftrightarrow ((⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩) \land ζ)$
72	70 71	mpbiran	$⊢ (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, F⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ζ) \leftrightarrow ζ$
73	67 72	bitrdi	$⊢ f = F \to ((⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨D, ⟨E, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land η) \leftrightarrow ζ)$
74	59 63 73	rspc3ev	$⊢ ((D \in Q \land E \in Q \land F \in Q) \land ζ) \to \exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land θ)$
75	74	3ad2antl3	$⊢ ((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 ζ) \to \exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land θ)$
76		opeq1	$⊢ a = A \to ⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨b, c⟩⟩$
77	76	eqeq1d	$⊢ a = A \to (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \leftrightarrow ⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩)$
78	77 1	3anbi13d	$⊢ a = A \to ((⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow (⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ψ))$
79	78	rexbidv	$⊢ a = A \to (\exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists f \in Q (⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ψ))$
80	79	2rexbidv	$⊢ a = A \to (\exists d \in Q \exists e \in Q \exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ψ))$
81		opeq1	$⊢ b = B \to ⟨b, c⟩ = ⟨B, c⟩$
82	81	opeq2d	$⊢ b = B \to ⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, c⟩⟩$
83	82	eqeq1d	$⊢ b = B \to (⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \leftrightarrow ⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩)$
84	83 2	3anbi13d	$⊢ b = B \to ((⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ψ) \leftrightarrow (⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land χ))$
85	84	rexbidv	$⊢ b = B \to (\exists f \in Q (⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ψ) \leftrightarrow \exists f \in Q (⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land χ))$
86	85	2rexbidv	$⊢ b = B \to (\exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land ψ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land χ))$
87		opeq2	$⊢ c = C \to ⟨B, c⟩ = ⟨B, C⟩$
88	87	opeq2d	$⊢ c = C \to ⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩$
89	88	eqeq1d	$⊢ c = C \to (⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \leftrightarrow ⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩)$
90	89 3	3anbi13d	$⊢ c = C \to ((⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land χ) \leftrightarrow (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land θ))$
91	90	rexbidv	$⊢ c = C \to (\exists f \in Q (⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land χ) \leftrightarrow \exists f \in Q (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land θ))$
92	91	2rexbidv	$⊢ c = C \to (\exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨B, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land χ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land θ))$
93	80 86 92	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 (⟨A, ⟨B, C⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ)$
94	56 75 93	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 ζ) \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ)$
95	7	rexeqdv	$⊢ x = X \to (\exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
96	7 95	rexeqbidv	$⊢ x = X \to (\exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists e \in Q \exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
97	7 96	rexeqbidv	$⊢ x = X \to (\exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists d \in Q \exists e \in Q \exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
98	7 97	rexeqbidv	$⊢ x = X \to (\exists c \in P \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
99	7 98	rexeqbidv	$⊢ x = X \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow \exists b \in Q \exists c \in Q \exists d \in Q \exists e \in Q \exists f \in Q (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
100	7 99	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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
101	100	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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ)$
102	55 94 101	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 ζ) \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ)$
103	102	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)) \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ))$
104	54 103	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)) \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 (⟨a, ⟨b, c⟩⟩ = ⟨A, ⟨B, C⟩⟩ \land ⟨d, ⟨e, f⟩⟩ = ⟨D, ⟨E, F⟩⟩ \land φ) \leftrightarrow ζ)$
105	27 104	syl5bb	$⊢ (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)) \to (⟨A, ⟨B, C⟩⟩ R ⟨D, ⟨E, F⟩⟩ \leftrightarrow ζ)$

Metamath Proof Explorer

Theorem br6

Proof