# Metamath Proof Explorer

## Theorem br4

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

Ref Expression
Hypotheses br4.1 ${⊢}{a}={A}\to \left({\phi }↔{\psi }\right)$
br4.2 ${⊢}{b}={B}\to \left({\psi }↔{\chi }\right)$
br4.3 ${⊢}{c}={C}\to \left({\chi }↔{\theta }\right)$
br4.4 ${⊢}{d}={D}\to \left({\theta }↔{\tau }\right)$
br4.5 ${⊢}{x}={X}\to {P}={Q}$
br4.6 ${⊢}{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}}\left({p}=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)\right\}$
Assertion br4 ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\to \left(⟨{A},{B}⟩{R}⟨{C},{D}⟩↔{\tau }\right)$

### Proof

Step Hyp Ref Expression
1 br4.1 ${⊢}{a}={A}\to \left({\phi }↔{\psi }\right)$
2 br4.2 ${⊢}{b}={B}\to \left({\psi }↔{\chi }\right)$
3 br4.3 ${⊢}{c}={C}\to \left({\chi }↔{\theta }\right)$
4 br4.4 ${⊢}{d}={D}\to \left({\theta }↔{\tau }\right)$
5 br4.5 ${⊢}{x}={X}\to {P}={Q}$
6 br4.6 ${⊢}{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}}\left({p}=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)\right\}$
7 opex ${⊢}⟨{A},{B}⟩\in \mathrm{V}$
8 opex ${⊢}⟨{C},{D}⟩\in \mathrm{V}$
9 eqeq1 ${⊢}{p}=⟨{A},{B}⟩\to \left({p}=⟨{a},{b}⟩↔⟨{A},{B}⟩=⟨{a},{b}⟩\right)$
10 9 3anbi1d ${⊢}{p}=⟨{A},{B}⟩\to \left(\left({p}=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)↔\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
11 10 rexbidv ${⊢}{p}=⟨{A},{B}⟩\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\left({p}=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)↔\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
12 11 2rexbidv ${⊢}{p}=⟨{A},{B}⟩\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}}\left({p}=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
13 12 2rexbidv ${⊢}{p}=⟨{A},{B}⟩\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}}\left({p}=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
14 eqeq1 ${⊢}{q}=⟨{C},{D}⟩\to \left({q}=⟨{c},{d}⟩↔⟨{C},{D}⟩=⟨{c},{d}⟩\right)$
15 14 3anbi2d ${⊢}{q}=⟨{C},{D}⟩\to \left(\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)↔\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
16 15 rexbidv ${⊢}{q}=⟨{C},{D}⟩\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\wedge {\phi }\right)↔\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
17 16 2rexbidv ${⊢}{q}=⟨{C},{D}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
18 17 2rexbidv ${⊢}{q}=⟨{C},{D}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge {q}=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
19 7 8 13 18 6 brab ${⊢}⟨{A},{B}⟩{R}⟨{C},{D}⟩↔\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)$
20 vex ${⊢}{a}\in \mathrm{V}$
21 vex ${⊢}{b}\in \mathrm{V}$
22 20 21 opth ${⊢}⟨{a},{b}⟩=⟨{A},{B}⟩↔\left({a}={A}\wedge {b}={B}\right)$
23 1 2 sylan9bb ${⊢}\left({a}={A}\wedge {b}={B}\right)\to \left({\phi }↔{\chi }\right)$
24 22 23 sylbi ${⊢}⟨{a},{b}⟩=⟨{A},{B}⟩\to \left({\phi }↔{\chi }\right)$
25 24 eqcoms ${⊢}⟨{A},{B}⟩=⟨{a},{b}⟩\to \left({\phi }↔{\chi }\right)$
26 vex ${⊢}{c}\in \mathrm{V}$
27 vex ${⊢}{d}\in \mathrm{V}$
28 26 27 opth ${⊢}⟨{c},{d}⟩=⟨{C},{D}⟩↔\left({c}={C}\wedge {d}={D}\right)$
29 3 4 sylan9bb ${⊢}\left({c}={C}\wedge {d}={D}\right)\to \left({\chi }↔{\tau }\right)$
30 28 29 sylbi ${⊢}⟨{c},{d}⟩=⟨{C},{D}⟩\to \left({\chi }↔{\tau }\right)$
31 30 eqcoms ${⊢}⟨{C},{D}⟩=⟨{c},{d}⟩\to \left({\chi }↔{\tau }\right)$
32 25 31 sylan9bb ${⊢}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\right)\to \left({\phi }↔{\tau }\right)$
33 32 biimp3a ${⊢}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\to {\tau }$
34 33 a1i ${⊢}\left(\left(\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\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 {d}\in {P}\right)\to \left(\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\to {\tau }\right)$
35 34 rexlimdva ${⊢}\left(\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\to {\tau }\right)$
36 35 rexlimdvva ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\to {\tau }\right)$
37 36 rexlimdvva ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\to {\tau }\right)$
38 simpl1 ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to {X}\in {S}$
39 simpl2l ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to {A}\in {Q}$
40 simpl2r ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to {B}\in {Q}$
41 simpl3l ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to {C}\in {Q}$
42 simpl3r ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to {D}\in {Q}$
43 eqidd ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to ⟨{A},{B}⟩=⟨{A},{B}⟩$
44 eqidd ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to ⟨{C},{D}⟩=⟨{C},{D}⟩$
45 simpr ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to {\tau }$
46 opeq1 ${⊢}{c}={C}\to ⟨{c},{d}⟩=⟨{C},{d}⟩$
47 46 eqeq2d ${⊢}{c}={C}\to \left(⟨{C},{D}⟩=⟨{c},{d}⟩↔⟨{C},{D}⟩=⟨{C},{d}⟩\right)$
48 47 3 3anbi23d ${⊢}{c}={C}\to \left(\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\chi }\right)↔\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{C},{d}⟩\wedge {\theta }\right)\right)$
49 opeq2 ${⊢}{d}={D}\to ⟨{C},{d}⟩=⟨{C},{D}⟩$
50 49 eqeq2d ${⊢}{d}={D}\to \left(⟨{C},{D}⟩=⟨{C},{d}⟩↔⟨{C},{D}⟩=⟨{C},{D}⟩\right)$
51 50 4 3anbi23d ${⊢}{d}={D}\to \left(\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{C},{d}⟩\wedge {\theta }\right)↔\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{C},{D}⟩\wedge {\tau }\right)\right)$
52 48 51 rspc2ev ${⊢}\left({C}\in {Q}\wedge {D}\in {Q}\wedge \left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{C},{D}⟩\wedge {\tau }\right)\right)\to \exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\chi }\right)$
53 41 42 43 44 45 52 syl113anc ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\right)\to \exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\chi }\right)$
54 opeq1 ${⊢}{a}={A}\to ⟨{a},{b}⟩=⟨{A},{b}⟩$
55 54 eqeq2d ${⊢}{a}={A}\to \left(⟨{A},{B}⟩=⟨{a},{b}⟩↔⟨{A},{B}⟩=⟨{A},{b}⟩\right)$
56 55 1 3anbi13d ${⊢}{a}={A}\to \left(\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)↔\left(⟨{A},{B}⟩=⟨{A},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\psi }\right)\right)$
57 56 2rexbidv ${⊢}{a}={A}\to \left(\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)↔\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{A},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\psi }\right)\right)$
58 opeq2 ${⊢}{b}={B}\to ⟨{A},{b}⟩=⟨{A},{B}⟩$
59 58 eqeq2d ${⊢}{b}={B}\to \left(⟨{A},{B}⟩=⟨{A},{b}⟩↔⟨{A},{B}⟩=⟨{A},{B}⟩\right)$
60 59 2 3anbi13d ${⊢}{b}={B}\to \left(\left(⟨{A},{B}⟩=⟨{A},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\psi }\right)↔\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\chi }\right)\right)$
61 60 2rexbidv ${⊢}{b}={B}\to \left(\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{A},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\psi }\right)↔\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\chi }\right)\right)$
62 57 61 rspc2ev ${⊢}\left({A}\in {Q}\wedge {B}\in {Q}\wedge \exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{A},{B}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\chi }\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)$
63 39 40 53 62 syl3anc ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)$
64 5 rexeqdv ${⊢}{x}={X}\to \left(\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)↔\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
65 5 64 rexeqbidv ${⊢}{x}={X}\to \left(\exists {c}\in {P}\phantom{\rule{.4em}{0ex}}\exists {d}\in {P}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)↔\exists {c}\in {Q}\phantom{\rule{.4em}{0ex}}\exists {d}\in {Q}\phantom{\rule{.4em}{0ex}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
66 5 65 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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
67 5 66 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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
68 67 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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)$
69 38 63 68 syl2anc ${⊢}\left(\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\wedge {\tau }\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)$
70 69 ex ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\to \left({\tau }\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)\right)$
71 37 70 impbid ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\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}}\left(⟨{A},{B}⟩=⟨{a},{b}⟩\wedge ⟨{C},{D}⟩=⟨{c},{d}⟩\wedge {\phi }\right)↔{\tau }\right)$
72 19 71 syl5bb ${⊢}\left({X}\in {S}\wedge \left({A}\in {Q}\wedge {B}\in {Q}\right)\wedge \left({C}\in {Q}\wedge {D}\in {Q}\right)\right)\to \left(⟨{A},{B}⟩{R}⟨{C},{D}⟩↔{\tau }\right)$