# Metamath Proof Explorer

## Theorem tpres

Description: An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020)

Ref Expression
Hypotheses tpres.t ${⊢}{\phi }\to {T}=\left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}$
tpres.b ${⊢}{\phi }\to {B}\in {V}$
tpres.c ${⊢}{\phi }\to {C}\in {V}$
tpres.e ${⊢}{\phi }\to {E}\in {V}$
tpres.f ${⊢}{\phi }\to {F}\in {V}$
tpres.1 ${⊢}{\phi }\to {B}\ne {A}$
tpres.2 ${⊢}{\phi }\to {C}\ne {A}$
Assertion tpres ${⊢}{\phi }\to {{T}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}$

### Proof

Step Hyp Ref Expression
1 tpres.t ${⊢}{\phi }\to {T}=\left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}$
2 tpres.b ${⊢}{\phi }\to {B}\in {V}$
3 tpres.c ${⊢}{\phi }\to {C}\in {V}$
4 tpres.e ${⊢}{\phi }\to {E}\in {V}$
5 tpres.f ${⊢}{\phi }\to {F}\in {V}$
6 tpres.1 ${⊢}{\phi }\to {B}\ne {A}$
7 tpres.2 ${⊢}{\phi }\to {C}\ne {A}$
8 df-res ${⊢}{{T}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}={T}\cap \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)$
9 elin ${⊢}{x}\in \left({T}\cap \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)\right)↔\left({x}\in {T}\wedge {x}\in \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)\right)$
10 elxp ${⊢}{x}\in \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)↔\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)$
11 10 anbi2i ${⊢}\left({x}\in {T}\wedge {x}\in \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)\right)↔\left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
12 1 eleq2d ${⊢}{\phi }\to \left({x}\in {T}↔{x}\in \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)$
13 vex ${⊢}{x}\in \mathrm{V}$
14 13 eltp ${⊢}{x}\in \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}↔\left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
15 eldifsn ${⊢}{a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)↔\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)$
16 eqeq1 ${⊢}{x}=⟨{a},{b}⟩\to \left({x}=⟨{A},{D}⟩↔⟨{a},{b}⟩=⟨{A},{D}⟩\right)$
17 16 adantl ${⊢}\left({a}\ne {A}\wedge {x}=⟨{a},{b}⟩\right)\to \left({x}=⟨{A},{D}⟩↔⟨{a},{b}⟩=⟨{A},{D}⟩\right)$
18 vex ${⊢}{a}\in \mathrm{V}$
19 vex ${⊢}{b}\in \mathrm{V}$
20 18 19 opth ${⊢}⟨{a},{b}⟩=⟨{A},{D}⟩↔\left({a}={A}\wedge {b}={D}\right)$
21 eqneqall ${⊢}{a}={A}\to \left({a}\ne {A}\to \left({b}={D}\to \left({\phi }\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)\right)$
22 21 com12 ${⊢}{a}\ne {A}\to \left({a}={A}\to \left({b}={D}\to \left({\phi }\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)\right)$
23 22 impd ${⊢}{a}\ne {A}\to \left(\left({a}={A}\wedge {b}={D}\right)\to \left({\phi }\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
24 20 23 syl5bi ${⊢}{a}\ne {A}\to \left(⟨{a},{b}⟩=⟨{A},{D}⟩\to \left({\phi }\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
25 24 adantr ${⊢}\left({a}\ne {A}\wedge {x}=⟨{a},{b}⟩\right)\to \left(⟨{a},{b}⟩=⟨{A},{D}⟩\to \left({\phi }\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
26 17 25 sylbid ${⊢}\left({a}\ne {A}\wedge {x}=⟨{a},{b}⟩\right)\to \left({x}=⟨{A},{D}⟩\to \left({\phi }\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
27 26 impd ${⊢}\left({a}\ne {A}\wedge {x}=⟨{a},{b}⟩\right)\to \left(\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
28 27 ex ${⊢}{a}\ne {A}\to \left({x}=⟨{a},{b}⟩\to \left(\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
29 28 adantl ${⊢}\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\to \left({x}=⟨{a},{b}⟩\to \left(\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
30 15 29 sylbi ${⊢}{a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\to \left({x}=⟨{a},{b}⟩\to \left(\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
31 30 adantr ${⊢}\left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\to \left({x}=⟨{a},{b}⟩\to \left(\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
32 31 impcom ${⊢}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to \left(\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
33 32 com12 ${⊢}\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left(\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
34 33 exlimdvv ${⊢}\left({x}=⟨{A},{D}⟩\wedge {\phi }\right)\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
35 34 ex ${⊢}{x}=⟨{A},{D}⟩\to \left({\phi }\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)\right)$
36 35 impd ${⊢}{x}=⟨{A},{D}⟩\to \left(\left({\phi }\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
37 orc ${⊢}{x}=⟨{B},{E}⟩\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
38 37 a1d ${⊢}{x}=⟨{B},{E}⟩\to \left(\left({\phi }\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
39 olc ${⊢}{x}=⟨{C},{F}⟩\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
40 39 a1d ${⊢}{x}=⟨{C},{F}⟩\to \left(\left({\phi }\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
41 36 38 40 3jaoi ${⊢}\left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\to \left(\left({\phi }\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
42 14 41 sylbi ${⊢}{x}\in \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\to \left(\left({\phi }\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to \left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
43 13 elpr ${⊢}{x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}↔\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
44 42 43 syl6ibr ${⊢}{x}\in \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\to \left(\left({\phi }\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to {x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)$
45 44 expd ${⊢}{x}\in \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\to \left({\phi }\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to {x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)\right)$
46 45 com12 ${⊢}{\phi }\to \left({x}\in \left\{⟨{A},{D}⟩,⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to {x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)\right)$
47 12 46 sylbid ${⊢}{\phi }\to \left({x}\in {T}\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\to {x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)\right)$
48 47 impd ${⊢}{\phi }\to \left(\left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\to {x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)$
49 3mix2 ${⊢}{x}=⟨{B},{E}⟩\to \left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
50 3mix3 ${⊢}{x}=⟨{C},{F}⟩\to \left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
51 49 50 jaoi ${⊢}\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\to \left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
52 51 adantr ${⊢}\left(\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\wedge {\phi }\right)\to \left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)$
53 12 14 syl6bb ${⊢}{\phi }\to \left({x}\in {T}↔\left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
54 53 adantl ${⊢}\left(\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\wedge {\phi }\right)\to \left({x}\in {T}↔\left({x}=⟨{A},{D}⟩\vee {x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\right)$
55 52 54 mpbird ${⊢}\left(\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\wedge {\phi }\right)\to {x}\in {T}$
56 2 elexd ${⊢}{\phi }\to {B}\in \mathrm{V}$
57 4 elexd ${⊢}{\phi }\to {E}\in \mathrm{V}$
58 56 6 57 jca31 ${⊢}{\phi }\to \left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)$
59 58 anim2i ${⊢}\left({x}=⟨{B},{E}⟩\wedge {\phi }\right)\to \left({x}=⟨{B},{E}⟩\wedge \left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)\right)$
60 opeq12 ${⊢}\left({a}={B}\wedge {b}={E}\right)\to ⟨{a},{b}⟩=⟨{B},{E}⟩$
61 60 eqeq2d ${⊢}\left({a}={B}\wedge {b}={E}\right)\to \left({x}=⟨{a},{b}⟩↔{x}=⟨{B},{E}⟩\right)$
62 eleq1 ${⊢}{a}={B}\to \left({a}\in \mathrm{V}↔{B}\in \mathrm{V}\right)$
63 neeq1 ${⊢}{a}={B}\to \left({a}\ne {A}↔{B}\ne {A}\right)$
64 62 63 anbi12d ${⊢}{a}={B}\to \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)↔\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\right)$
65 eleq1 ${⊢}{b}={E}\to \left({b}\in \mathrm{V}↔{E}\in \mathrm{V}\right)$
66 64 65 bi2anan9 ${⊢}\left({a}={B}\wedge {b}={E}\right)\to \left(\left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)↔\left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)\right)$
67 61 66 anbi12d ${⊢}\left({a}={B}\wedge {b}={E}\right)\to \left(\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)↔\left({x}=⟨{B},{E}⟩\wedge \left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)\right)\right)$
68 67 spc2egv ${⊢}\left({B}\in {V}\wedge {E}\in {V}\right)\to \left(\left({x}=⟨{B},{E}⟩\wedge \left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
69 2 4 68 syl2anc ${⊢}{\phi }\to \left(\left({x}=⟨{B},{E}⟩\wedge \left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
70 69 adantl ${⊢}\left({x}=⟨{B},{E}⟩\wedge {\phi }\right)\to \left(\left({x}=⟨{B},{E}⟩\wedge \left(\left({B}\in \mathrm{V}\wedge {B}\ne {A}\right)\wedge {E}\in \mathrm{V}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
71 59 70 mpd ${⊢}\left({x}=⟨{B},{E}⟩\wedge {\phi }\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)$
72 3 elexd ${⊢}{\phi }\to {C}\in \mathrm{V}$
73 5 elexd ${⊢}{\phi }\to {F}\in \mathrm{V}$
74 72 7 73 jca31 ${⊢}{\phi }\to \left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)$
75 74 anim2i ${⊢}\left({x}=⟨{C},{F}⟩\wedge {\phi }\right)\to \left({x}=⟨{C},{F}⟩\wedge \left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)\right)$
76 opeq12 ${⊢}\left({a}={C}\wedge {b}={F}\right)\to ⟨{a},{b}⟩=⟨{C},{F}⟩$
77 76 eqeq2d ${⊢}\left({a}={C}\wedge {b}={F}\right)\to \left({x}=⟨{a},{b}⟩↔{x}=⟨{C},{F}⟩\right)$
78 eleq1 ${⊢}{a}={C}\to \left({a}\in \mathrm{V}↔{C}\in \mathrm{V}\right)$
79 neeq1 ${⊢}{a}={C}\to \left({a}\ne {A}↔{C}\ne {A}\right)$
80 78 79 anbi12d ${⊢}{a}={C}\to \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)↔\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\right)$
81 eleq1 ${⊢}{b}={F}\to \left({b}\in \mathrm{V}↔{F}\in \mathrm{V}\right)$
82 80 81 bi2anan9 ${⊢}\left({a}={C}\wedge {b}={F}\right)\to \left(\left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)↔\left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)\right)$
83 77 82 anbi12d ${⊢}\left({a}={C}\wedge {b}={F}\right)\to \left(\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)↔\left({x}=⟨{C},{F}⟩\wedge \left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)\right)\right)$
84 83 spc2egv ${⊢}\left({C}\in {V}\wedge {F}\in {V}\right)\to \left(\left({x}=⟨{C},{F}⟩\wedge \left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
85 3 5 84 syl2anc ${⊢}{\phi }\to \left(\left({x}=⟨{C},{F}⟩\wedge \left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
86 85 adantl ${⊢}\left({x}=⟨{C},{F}⟩\wedge {\phi }\right)\to \left(\left({x}=⟨{C},{F}⟩\wedge \left(\left({C}\in \mathrm{V}\wedge {C}\ne {A}\right)\wedge {F}\in \mathrm{V}\right)\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
87 75 86 mpd ${⊢}\left({x}=⟨{C},{F}⟩\wedge {\phi }\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)$
88 71 87 jaoian ${⊢}\left(\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\wedge {\phi }\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)$
89 15 anbi1i ${⊢}\left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)↔\left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)$
90 89 anbi2i ${⊢}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)↔\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)$
91 90 2exbii ${⊢}\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)↔\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left(\left({a}\in \mathrm{V}\wedge {a}\ne {A}\right)\wedge {b}\in \mathrm{V}\right)\right)$
92 88 91 sylibr ${⊢}\left(\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\wedge {\phi }\right)\to \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)$
93 55 92 jca ${⊢}\left(\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\wedge {\phi }\right)\to \left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)$
94 93 ex ${⊢}\left({x}=⟨{B},{E}⟩\vee {x}=⟨{C},{F}⟩\right)\to \left({\phi }\to \left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\right)$
95 43 94 sylbi ${⊢}{x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\to \left({\phi }\to \left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\right)$
96 95 com12 ${⊢}{\phi }\to \left({x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\to \left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)\right)$
97 48 96 impbid ${⊢}{\phi }\to \left(\left({x}\in {T}\wedge \exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{a},{b}⟩\wedge \left({a}\in \left(\mathrm{V}\setminus \left\{{A}\right\}\right)\wedge {b}\in \mathrm{V}\right)\right)\right)↔{x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)$
98 11 97 syl5bb ${⊢}{\phi }\to \left(\left({x}\in {T}\wedge {x}\in \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)\right)↔{x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)$
99 9 98 syl5bb ${⊢}{\phi }\to \left({x}\in \left({T}\cap \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)\right)↔{x}\in \left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}\right)$
100 99 eqrdv ${⊢}{\phi }\to {T}\cap \left(\left(\mathrm{V}\setminus \left\{{A}\right\}\right)×\mathrm{V}\right)=\left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}$
101 8 100 syl5eq ${⊢}{\phi }\to {{T}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left\{⟨{B},{E}⟩,⟨{C},{F}⟩\right\}$