Metamath Proof Explorer

Theorem 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 \left({\phi }↔{\psi }\right)$
br6.2 ${⊢}{b}={B}\to \left({\psi }↔{\chi }\right)$
br6.3 ${⊢}{c}={C}\to \left({\chi }↔{\theta }\right)$
br6.4 ${⊢}{d}={D}\to \left({\theta }↔{\tau }\right)$
br6.5 ${⊢}{e}={E}\to \left({\tau }↔{\eta }\right)$
br6.6 ${⊢}{f}={F}\to \left({\eta }↔{\zeta }\right)$
br6.7 ${⊢}{x}={X}\to {P}={Q}$
br6.8 ${⊢}{R}=\left\{⟨{p},{q}⟩|\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right\}$
Assertion br6 ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩{R}⟨{D},⟨{E},{F}⟩⟩↔{\zeta }\right)$

Proof

Step Hyp Ref Expression
1 br6.1 ${⊢}{a}={A}\to \left({\phi }↔{\psi }\right)$
2 br6.2 ${⊢}{b}={B}\to \left({\psi }↔{\chi }\right)$
3 br6.3 ${⊢}{c}={C}\to \left({\chi }↔{\theta }\right)$
4 br6.4 ${⊢}{d}={D}\to \left({\theta }↔{\tau }\right)$
5 br6.5 ${⊢}{e}={E}\to \left({\tau }↔{\eta }\right)$
6 br6.6 ${⊢}{f}={F}\to \left({\eta }↔{\zeta }\right)$
7 br6.7 ${⊢}{x}={X}\to {P}={Q}$
8 br6.8 ${⊢}{R}=\left\{⟨{p},{q}⟩|\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right\}$
9 opex ${⊢}⟨{A},⟨{B},{C}⟩⟩\in \mathrm{V}$
10 opex ${⊢}⟨{D},⟨{E},{F}⟩⟩\in \mathrm{V}$
11 eqeq1 ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left({p}=⟨{a},⟨{b},{c}⟩⟩↔⟨{A},⟨{B},{C}⟩⟩=⟨{a},⟨{b},{c}⟩⟩\right)$
12 eqcom ${⊢}⟨{A},⟨{B},{C}⟩⟩=⟨{a},⟨{b},{c}⟩⟩↔⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩$
13 11 12 syl6bb ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left({p}=⟨{a},⟨{b},{c}⟩⟩↔⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\right)$
14 13 3anbi1d ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left(\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right)$
15 14 rexbidv ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left(\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right)$
16 15 2rexbidv ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right)$
17 16 2rexbidv ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left(\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right)$
18 17 2rexbidv ${⊢}{p}=⟨{A},⟨{B},{C}⟩⟩\to \left(\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},⟨{b},{c}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)\right)$
19 eqeq1 ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left({q}=⟨{d},⟨{e},{f}⟩⟩↔⟨{D},⟨{E},{F}⟩⟩=⟨{d},⟨{e},{f}⟩⟩\right)$
20 eqcom ${⊢}⟨{D},⟨{E},{F}⟩⟩=⟨{d},⟨{e},{f}⟩⟩↔⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩$
21 19 20 syl6bb ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left({q}=⟨{d},⟨{e},{f}⟩⟩↔⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)$
22 21 3anbi2d ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left(\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
23 22 rexbidv ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left(\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
24 23 2rexbidv ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
25 24 2rexbidv ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left(\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
26 25 2rexbidv ${⊢}{q}=⟨{D},⟨{E},{F}⟩⟩\to \left(\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge {q}=⟨{d},⟨{e},{f}⟩⟩\wedge {\phi }\right)↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
27 9 10 18 26 8 brab ${⊢}⟨{A},⟨{B},{C}⟩⟩{R}⟨{D},⟨{E},{F}⟩⟩↔\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)$
28 vex ${⊢}{a}\in \mathrm{V}$
29 opex ${⊢}⟨{b},{c}⟩\in \mathrm{V}$
30 28 29 opth ${⊢}⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩↔\left({a}={A}\wedge ⟨{b},{c}⟩=⟨{B},{C}⟩\right)$
31 vex ${⊢}{b}\in \mathrm{V}$
32 vex ${⊢}{c}\in \mathrm{V}$
33 31 32 opth ${⊢}⟨{b},{c}⟩=⟨{B},{C}⟩↔\left({b}={B}\wedge {c}={C}\right)$
34 2 3 sylan9bb ${⊢}\left({b}={B}\wedge {c}={C}\right)\to \left({\psi }↔{\theta }\right)$
35 33 34 sylbi ${⊢}⟨{b},{c}⟩=⟨{B},{C}⟩\to \left({\psi }↔{\theta }\right)$
36 1 35 sylan9bb ${⊢}\left({a}={A}\wedge ⟨{b},{c}⟩=⟨{B},{C}⟩\right)\to \left({\phi }↔{\theta }\right)$
37 30 36 sylbi ${⊢}⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\to \left({\phi }↔{\theta }\right)$
38 vex ${⊢}{d}\in \mathrm{V}$
39 opex ${⊢}⟨{e},{f}⟩\in \mathrm{V}$
40 38 39 opth ${⊢}⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩↔\left({d}={D}\wedge ⟨{e},{f}⟩=⟨{E},{F}⟩\right)$
41 vex ${⊢}{e}\in \mathrm{V}$
42 vex ${⊢}{f}\in \mathrm{V}$
43 41 42 opth ${⊢}⟨{e},{f}⟩=⟨{E},{F}⟩↔\left({e}={E}\wedge {f}={F}\right)$
44 5 6 sylan9bb ${⊢}\left({e}={E}\wedge {f}={F}\right)\to \left({\tau }↔{\zeta }\right)$
45 43 44 sylbi ${⊢}⟨{e},{f}⟩=⟨{E},{F}⟩\to \left({\tau }↔{\zeta }\right)$
46 4 45 sylan9bb ${⊢}\left({d}={D}\wedge ⟨{e},{f}⟩=⟨{E},{F}⟩\right)\to \left({\theta }↔{\zeta }\right)$
47 40 46 sylbi ${⊢}⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\to \left({\theta }↔{\zeta }\right)$
48 37 47 sylan9bb ${⊢}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)\to \left({\phi }↔{\zeta }\right)$
49 48 biimp3a ${⊢}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\to {\zeta }$
50 49 a1i ${⊢}\left(\left(\left(\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge \left({x}\in {S}\wedge {a}\in {P}\right)\right)\wedge \left({b}\in {P}\wedge {c}\in {P}\right)\right)\wedge \left({d}\in {P}\wedge {e}\in {P}\right)\right)\wedge {f}\in {P}\right)\to \left(\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\to {\zeta }\right)$
51 50 rexlimdva ${⊢}\left(\left(\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge \left({x}\in {S}\wedge {a}\in {P}\right)\right)\wedge \left({b}\in {P}\wedge {c}\in {P}\right)\right)\wedge \left({d}\in {P}\wedge {e}\in {P}\right)\right)\to \left(\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\to {\zeta }\right)$
52 51 rexlimdvva ${⊢}\left(\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge \left({x}\in {S}\wedge {a}\in {P}\right)\right)\wedge \left({b}\in {P}\wedge {c}\in {P}\right)\right)\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\to {\zeta }\right)$
53 52 rexlimdvva ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge \left({x}\in {S}\wedge {a}\in {P}\right)\right)\to \left(\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\to {\zeta }\right)$
54 53 rexlimdvva ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\to \left(\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\to {\zeta }\right)$
55 simpl1 ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge {\zeta }\right)\to {X}\in {S}$
56 simpl2 ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge {\zeta }\right)\to \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)$
57 opeq1 ${⊢}{d}={D}\to ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{e},{f}⟩⟩$
58 57 eqeq1d ${⊢}{d}={D}\to \left(⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩↔⟨{D},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)$
59 58 4 3anbi23d ${⊢}{d}={D}\to \left(\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)↔\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\tau }\right)\right)$
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 \left(⟨{D},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩↔⟨{D},⟨{E},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)$
63 62 5 3anbi23d ${⊢}{e}={E}\to \left(\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\tau }\right)↔\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\eta }\right)\right)$
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 \left(⟨{D},⟨{E},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩↔⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)$
67 66 6 3anbi23d ${⊢}{f}={F}\to \left(\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\eta }\right)↔\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\zeta }\right)\right)$
68 eqid ${⊢}⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩$
69 eqid ${⊢}⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩$
70 68 69 pm3.2i ${⊢}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)$
71 df-3an ${⊢}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\zeta }\right)↔\left(\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\right)\wedge {\zeta }\right)$
72 70 71 mpbiran ${⊢}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{F}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\zeta }\right)↔{\zeta }$
73 67 72 syl6bb ${⊢}{f}={F}\to \left(\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{D},⟨{E},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\eta }\right)↔{\zeta }\right)$
74 59 63 73 rspc3ev ${⊢}\left(\left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\wedge {\zeta }\right)\to \exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)$
75 74 3ad2antl3 ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge {\zeta }\right)\to \exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)$
76 opeq1 ${⊢}{a}={A}\to ⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{b},{c}⟩⟩$
77 76 eqeq1d ${⊢}{a}={A}\to \left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩↔⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\right)$
78 77 1 3anbi13d ${⊢}{a}={A}\to \left(\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\psi }\right)\right)$
79 78 rexbidv ${⊢}{a}={A}\to \left(\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\psi }\right)\right)$
80 79 2rexbidv ${⊢}{a}={A}\to \left(\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\psi }\right)\right)$
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 \left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩↔⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\right)$
84 83 2 3anbi13d ${⊢}{b}={B}\to \left(\left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\psi }\right)↔\left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\chi }\right)\right)$
85 84 rexbidv ${⊢}{b}={B}\to \left(\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\psi }\right)↔\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\chi }\right)\right)$
86 85 2rexbidv ${⊢}{b}={B}\to \left(\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\psi }\right)↔\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\chi }\right)\right)$
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 \left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩↔⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\right)$
90 89 3 3anbi13d ${⊢}{c}={C}\to \left(\left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\chi }\right)↔\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)\right)$
91 90 rexbidv ${⊢}{c}={C}\to \left(\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\chi }\right)↔\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)\right)$
92 91 2rexbidv ${⊢}{c}={C}\to \left(\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\chi }\right)↔\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)\right)$
93 80 86 92 rspc3ev ${⊢}\left(\left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},⟨{B},{C}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\theta }\right)\right)\to \exists {a}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {b}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)$
94 56 75 93 syl2anc ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge {\zeta }\right)\to \exists {a}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {b}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)$
95 7 rexeqdv ${⊢}{x}={X}\to \left(\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
96 7 95 rexeqbidv ${⊢}{x}={X}\to \left(\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
97 7 96 rexeqbidv ${⊢}{x}={X}\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
98 7 97 rexeqbidv ${⊢}{x}={X}\to \left(\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
99 7 98 rexeqbidv ${⊢}{x}={X}\to \left(\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {b}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
100 7 99 rexeqbidv ${⊢}{x}={X}\to \left(\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔\exists {a}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {b}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
101 100 rspcev ${⊢}\left({X}\in {S}\wedge \exists {a}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {b}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {e}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {f}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)$
102 55 94 101 syl2anc ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\wedge {\zeta }\right)\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)$
103 102 ex ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\to \left({\zeta }\to \exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)\right)$
104 54 103 impbid ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\to \left(\exists {x}\in {S}\phantom{\rule{.4em}{0ex}}\exists {a}\in {P}\phantom{\rule{.4em}{0ex}}\exists {b}\in {P}\phantom{\rule{.4em}{0ex}}\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\exists {e}\in {P}\phantom{\rule{.4em}{0ex}}\exists {f}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{a},⟨{b},{c}⟩⟩=⟨{A},⟨{B},{C}⟩⟩\wedge ⟨{d},⟨{e},{f}⟩⟩=⟨{D},⟨{E},{F}⟩⟩\wedge {\phi }\right)↔{\zeta }\right)$
105 27 104 syl5bb ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\wedge {C}\in {Q}\right)\wedge \left({D}\in {Q}\wedge {E}\in {Q}\wedge {F}\in {Q}\right)\right)\to \left(⟨{A},⟨{B},{C}⟩⟩{R}⟨{D},⟨{E},{F}⟩⟩↔{\zeta }\right)$