Metamath Proof Explorer

Theorem 2reu8i

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, see also 2reu8 . The involved wffs depend on the setvar variables as follows: ph(x,y), ta(v,y), ch(x,w), th(v,w), et(x,b), ps(a,b), ze(a,w). (Contributed by AV, 1-Apr-2023)

Ref Expression
Hypotheses 2reu8i.x ⊢ ( 𝑥 = 𝑣 → ( 𝜑 ↔ 𝜏 ) )
2reu8i.v ⊢ ( 𝑥 = 𝑣 → ( 𝜒 ↔ 𝜃 ) )
2reu8i.w ⊢ ( 𝑦 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
2reu8i.b ⊢ ( 𝑦 = 𝑏 → ( 𝜑 ↔ 𝜂 ) )
2reu8i.a ⊢ ( 𝑥 = 𝑎 → ( 𝜒 ↔ 𝜁 ) )
2reu8i.1 ⊢ ( ( ( 𝜒 → 𝑦 = 𝑤 ) ∧ 𝜁 ) → 𝑦 = 𝑤 )
2reu8i.2 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion 2reu8i ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 2reu8i.x ⊢ ( 𝑥 = 𝑣 → ( 𝜑 ↔ 𝜏 ) )
2 2reu8i.v ⊢ ( 𝑥 = 𝑣 → ( 𝜒 ↔ 𝜃 ) )
3 2reu8i.w ⊢ ( 𝑦 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
4 2reu8i.b ⊢ ( 𝑦 = 𝑏 → ( 𝜑 ↔ 𝜂 ) )
5 2reu8i.a ⊢ ( 𝑥 = 𝑎 → ( 𝜒 ↔ 𝜁 ) )
6 2reu8i.1 ⊢ ( ( ( 𝜒 → 𝑦 = 𝑤 ) ∧ 𝜁 ) → 𝑦 = 𝑤 )
7 2reu8i.2 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜑 ↔ 𝜓 ) )
8 3 reu8 ⊢ ( ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) )
9 8 reubii ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) )
10 2 imbi1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝜒 → 𝑦 = 𝑤 ) ↔ ( 𝜃 → 𝑦 = 𝑤 ) ) )
11 10 ralbidv ⊢ ( 𝑥 = 𝑣 → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) )
12 1 11 anbi12d ⊢ ( 𝑥 = 𝑣 → ( ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ↔ ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) ) )
13 12 rexbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) ) )
14 13 reu8 ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) )
15 9 14 bitri ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) )
16 nfv ⊢ Ⅎ 𝑢 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) )
17 nfs1v ⊢ Ⅎ 𝑦 [ 𝑢 / 𝑦 ] 𝜏
18 nfcv ⊢ Ⅎ 𝑦 𝐵
19 nfs1v ⊢ Ⅎ 𝑦 [ 𝑢 / 𝑦 ] 𝜃
20 nfv ⊢ Ⅎ 𝑦 𝑢 = 𝑤
21 19 20 nfim ⊢ Ⅎ 𝑦 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 )
22 18 21 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 )
23 17 22 nfan ⊢ Ⅎ 𝑦 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) )
24 sbequ12 ⊢ ( 𝑦 = 𝑢 → ( 𝜏 ↔ [ 𝑢 / 𝑦 ] 𝜏 ) )
25 sbequ12 ⊢ ( 𝑦 = 𝑢 → ( 𝜃 ↔ [ 𝑢 / 𝑦 ] 𝜃 ) )
26 equequ1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 = 𝑤 ↔ 𝑢 = 𝑤 ) )
27 25 26 imbi12d ⊢ ( 𝑦 = 𝑢 → ( ( 𝜃 → 𝑦 = 𝑤 ) ↔ ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) )
28 27 ralbidv ⊢ ( 𝑦 = 𝑢 → ( ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) )
29 24 28 anbi12d ⊢ ( 𝑦 = 𝑢 → ( ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) ↔ ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ) )
30 16 23 29 cbvrexw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) ↔ ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) )
31 30 imbi1i ⊢ ( ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ↔ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) )
32 31 ralbii ⊢ ( ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ↔ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) )
33 32 anbi2i ⊢ ( ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) )
34 nfcv ⊢ Ⅎ 𝑦 𝐴
35 18 23 nfrex ⊢ Ⅎ 𝑦 ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) )
36 nfv ⊢ Ⅎ 𝑦 𝑥 = 𝑣
37 35 36 nfim ⊢ Ⅎ 𝑦 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 )
38 34 37 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 )
39 38 r19.41 ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ↔ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) )
40 33 39 bitr4i ⊢ ( ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ↔ ∃ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) )
41 r19.28v ⊢ ( ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) )
42 simplr ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ) → 𝜑 )
43 nfv ⊢ Ⅎ 𝑣 ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 )
44 nfcv ⊢ Ⅎ 𝑣 𝐵
45 nfs1v ⊢ Ⅎ 𝑣 [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏
46 nfs1v ⊢ Ⅎ 𝑣 [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃
47 nfv ⊢ Ⅎ 𝑣 𝑢 = 𝑤
48 46 47 nfim ⊢ Ⅎ 𝑣 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 )
49 44 48 nfralw ⊢ Ⅎ 𝑣 ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 )
50 45 49 nfan ⊢ Ⅎ 𝑣 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) )
51 44 50 nfrex ⊢ Ⅎ 𝑣 ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) )
52 nfv ⊢ Ⅎ 𝑣 𝑥 = 𝑎
53 51 52 nfim ⊢ Ⅎ 𝑣 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 )
54 43 53 nfan ⊢ Ⅎ 𝑣 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) )
55 sbequ12 ⊢ ( 𝑣 = 𝑎 → ( [ 𝑢 / 𝑦 ] 𝜏 ↔ [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ) )
56 sbequ12 ⊢ ( 𝑣 = 𝑎 → ( [ 𝑢 / 𝑦 ] 𝜃 ↔ [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 ) )
57 56 imbi1d ⊢ ( 𝑣 = 𝑎 → ( ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ↔ ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) )
58 57 ralbidv ⊢ ( 𝑣 = 𝑎 → ( ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) )
59 55 58 anbi12d ⊢ ( 𝑣 = 𝑎 → ( ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ↔ ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ) )
60 59 rexbidv ⊢ ( 𝑣 = 𝑎 → ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ↔ ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ) )
61 equequ2 ⊢ ( 𝑣 = 𝑎 → ( 𝑥 = 𝑣 ↔ 𝑥 = 𝑎 ) )
62 60 61 imbi12d ⊢ ( 𝑣 = 𝑎 → ( ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ↔ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) )
63 62 anbi2d ⊢ ( 𝑣 = 𝑎 → ( ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) ) )
64 54 63 rspc ⊢ ( 𝑎 ∈ 𝐴 → ( ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) ) )
65 64 ad2antrl ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) ) )
66 nfs1v ⊢ Ⅎ 𝑤 [ 𝑏 / 𝑤 ] 𝜒
67 nfv ⊢ Ⅎ 𝑤 𝑦 = 𝑏
68 66 67 nfim ⊢ Ⅎ 𝑤 ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 )
69 sbequ12 ⊢ ( 𝑤 = 𝑏 → ( 𝜒 ↔ [ 𝑏 / 𝑤 ] 𝜒 ) )
70 equequ2 ⊢ ( 𝑤 = 𝑏 → ( 𝑦 = 𝑤 ↔ 𝑦 = 𝑏 ) )
71 69 70 imbi12d ⊢ ( 𝑤 = 𝑏 → ( ( 𝜒 → 𝑦 = 𝑤 ) ↔ ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) ) )
72 68 71 rspc ⊢ ( 𝑏 ∈ 𝐵 → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) ) )
73 72 adantl ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) ) )
74 73 adantl ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) ) )
75 74 imp ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) → ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) )
76 3 sbievw ⊢ ( [ 𝑤 / 𝑦 ] 𝜑 ↔ 𝜒 )
77 76 bicomi ⊢ ( 𝜒 ↔ [ 𝑤 / 𝑦 ] 𝜑 )
78 77 sbbii ⊢ ( [ 𝑏 / 𝑤 ] 𝜒 ↔ [ 𝑏 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
79 sbco2vv ⊢ ( [ 𝑏 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 )
80 78 79 bitri ⊢ ( [ 𝑏 / 𝑤 ] 𝜒 ↔ [ 𝑏 / 𝑦 ] 𝜑 )
81 80 imbi1i ⊢ ( ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) ↔ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) )
82 4 sbievw ⊢ ( [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜂 )
83 pm3.35 ⊢ ( ( [ 𝑏 / 𝑦 ] 𝜑 ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → 𝑦 = 𝑏 )
84 83 equcomd ⊢ ( ( [ 𝑏 / 𝑦 ] 𝜑 ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → 𝑏 = 𝑦 )
85 84 ex ⊢ ( [ 𝑏 / 𝑦 ] 𝜑 → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → 𝑏 = 𝑦 ) )
86 82 85 sylbir ⊢ ( 𝜂 → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → 𝑏 = 𝑦 ) )
87 86 com12 ⊢ ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → ( 𝜂 → 𝑏 = 𝑦 ) )
88 87 ad2antlr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) → ( 𝜂 → 𝑏 = 𝑦 ) )
89 simplrr ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) → 𝑏 ∈ 𝐵 )
90 89 ad2antrr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → 𝑏 ∈ 𝐵 )
91 sbequ ⊢ ( 𝑢 = 𝑏 → ( [ 𝑢 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 ) )
92 91 sbbidv ⊢ ( 𝑢 = 𝑏 → ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ) )
93 equequ1 ⊢ ( 𝑢 = 𝑏 → ( 𝑢 = 𝑤 ↔ 𝑏 = 𝑤 ) )
94 93 imbi2d ⊢ ( 𝑢 = 𝑏 → ( ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) )
95 94 ralbidv ⊢ ( 𝑢 = 𝑏 → ( ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) )
96 92 95 anbi12d ⊢ ( 𝑢 = 𝑏 → ( ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) ) )
97 96 adantl ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ 𝑢 = 𝑏 ) → ( ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) ) )
98 vex ⊢ 𝑎 ∈ V
99 vex ⊢ 𝑏 ∈ V
100 98 99 7 sbc2ie ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜓 )
101 100 a1i ⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ 𝜓 ) )
102 101 biimprd ⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → ( 𝜓 → [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ) )
103 102 adantld ⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → ( ( 𝜂 ∧ 𝜓 ) → [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ) )
104 103 imp ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
105 sbsbc ⊢ ( [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑏 / 𝑦 ] 𝜑 )
106 105 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
107 sbsbc ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
108 106 107 bitri ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
109 104 108 sylibr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 )
110 76 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] 𝜒 )
111 5 sbievw ⊢ ( [ 𝑎 / 𝑥 ] 𝜒 ↔ 𝜁 )
112 110 111 bitri ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ 𝜁 )
113 6 ex ⊢ ( ( 𝜒 → 𝑦 = 𝑤 ) → ( 𝜁 → 𝑦 = 𝑤 ) )
114 113 adantl ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝜒 → 𝑦 = 𝑤 ) ) → ( 𝜁 → 𝑦 = 𝑤 ) )
115 82 imbi1i ⊢ ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ↔ ( 𝜂 → 𝑦 = 𝑏 ) )
116 pm2.27 ⊢ ( 𝜂 → ( ( 𝜂 → 𝑦 = 𝑏 ) → 𝑦 = 𝑏 ) )
117 116 ad2antrl ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ( ( 𝜂 → 𝑦 = 𝑏 ) → 𝑦 = 𝑏 ) )
118 115 117 syl5bi ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → 𝑦 = 𝑏 ) )
119 ax7 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 = 𝑤 → 𝑏 = 𝑤 ) )
120 118 119 syl6 ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → ( 𝑦 = 𝑤 → 𝑏 = 𝑤 ) ) )
121 120 imp ⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → ( 𝑦 = 𝑤 → 𝑏 = 𝑤 ) )
122 121 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝜒 → 𝑦 = 𝑤 ) ) → ( 𝑦 = 𝑤 → 𝑏 = 𝑤 ) )
123 114 122 syld ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝜒 → 𝑦 = 𝑤 ) ) → ( 𝜁 → 𝑏 = 𝑤 ) )
124 112 123 syl5bi ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( 𝜒 → 𝑦 = 𝑤 ) ) → ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) )
125 124 ex ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ( 𝜒 → 𝑦 = 𝑤 ) → ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) )
126 125 ralimdva ⊢ ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) )
127 126 exp31 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝜂 ∧ 𝜓 ) → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) ) ) )
128 127 com24 ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → ( ( 𝜂 ∧ 𝜓 ) → ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) ) ) )
129 128 imp41 ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) )
130 109 129 jca ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑏 = 𝑤 ) ) )
131 90 97 130 rspcedvd ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ) )
132 1 sbievw ⊢ ( [ 𝑣 / 𝑥 ] 𝜑 ↔ 𝜏 )
133 132 bicomi ⊢ ( 𝜏 ↔ [ 𝑣 / 𝑥 ] 𝜑 )
134 133 sbbii ⊢ ( [ 𝑢 / 𝑦 ] 𝜏 ↔ [ 𝑢 / 𝑦 ] [ 𝑣 / 𝑥 ] 𝜑 )
135 sbcom2 ⊢ ( [ 𝑢 / 𝑦 ] [ 𝑣 / 𝑥 ] 𝜑 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 )
136 134 135 bitri ⊢ ( [ 𝑢 / 𝑦 ] 𝜏 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 )
137 136 sbbii ⊢ ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ↔ [ 𝑎 / 𝑣 ] [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 )
138 sbco2vv ⊢ ( [ 𝑎 / 𝑣 ] [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 )
139 137 138 bitri ⊢ ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ↔ [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 )
140 2 sbievw ⊢ ( [ 𝑣 / 𝑥 ] 𝜒 ↔ 𝜃 )
141 140 bicomi ⊢ ( 𝜃 ↔ [ 𝑣 / 𝑥 ] 𝜒 )
142 141 sbbii ⊢ ( [ 𝑢 / 𝑦 ] 𝜃 ↔ [ 𝑢 / 𝑦 ] [ 𝑣 / 𝑥 ] 𝜒 )
143 sbcom2 ⊢ ( [ 𝑢 / 𝑦 ] [ 𝑣 / 𝑥 ] 𝜒 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 )
144 142 143 bitri ⊢ ( [ 𝑢 / 𝑦 ] 𝜃 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 )
145 144 sbbii ⊢ ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 ↔ [ 𝑎 / 𝑣 ] [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 )
146 sbco2vv ⊢ ( [ 𝑎 / 𝑣 ] [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 ↔ [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 )
147 77 sbbii ⊢ ( [ 𝑢 / 𝑦 ] 𝜒 ↔ [ 𝑢 / 𝑦 ] [ 𝑤 / 𝑦 ] 𝜑 )
148 nfs1v ⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
149 148 sbf ⊢ ( [ 𝑢 / 𝑦 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] 𝜑 )
150 147 149 bitri ⊢ ( [ 𝑢 / 𝑦 ] 𝜒 ↔ [ 𝑤 / 𝑦 ] 𝜑 )
151 150 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜒 ↔ [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
152 145 146 151 3bitri ⊢ ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 ↔ [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
153 152 imbi1i ⊢ ( ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) )
154 153 ralbii ⊢ ( ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) )
155 139 154 anbi12i ⊢ ( ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ↔ ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ) )
156 155 rexbii ⊢ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) ↔ ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → 𝑢 = 𝑤 ) ) )
157 131 156 sylibr ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) )
158 pm2.27 ⊢ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → ( ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) → 𝑥 = 𝑎 ) )
159 157 158 syl ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → ( ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) → 𝑥 = 𝑎 ) )
160 159 impancom ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) → ( ( 𝜂 ∧ 𝜓 ) → 𝑥 = 𝑎 ) )
161 160 imp ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → 𝑥 = 𝑎 )
162 161 equcomd ⊢ ( ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) ∧ ( 𝜂 ∧ 𝜓 ) ) → 𝑎 = 𝑥 )
163 162 exp32 ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) → ( 𝜂 → ( 𝜓 → 𝑎 = 𝑥 ) ) )
164 88 163 jcad ⊢ ( ( ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) )
165 164 exp31 ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) → ( ( [ 𝑏 / 𝑦 ] 𝜑 → 𝑦 = 𝑏 ) → ( ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
166 81 165 syl5bi ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) → ( ( [ 𝑏 / 𝑤 ] 𝜒 → 𝑦 = 𝑏 ) → ( ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
167 75 166 mpd ⊢ ( ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) → ( ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )
168 167 expimpd ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑎 / 𝑣 ] [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑎 ) ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )
169 65 168 syld ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )
170 169 impancom ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )
171 170 ralrimivv ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) )
172 42 171 jca ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) ) → ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )
173 172 ex ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → ( ∀ 𝑣 ∈ 𝐴 ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
174 41 173 syl5 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → ( ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
175 174 expd ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → ( ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) → ( ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) → ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) ) )
176 175 expimpd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) → ( ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) → ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) ) )
177 176 impd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
178 177 reximdva ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑢 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( [ 𝑢 / 𝑦 ] 𝜃 → 𝑢 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
179 40 178 syl5bi ⊢ ( 𝑥 ∈ 𝐴 → ( ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) ) )
180 179 reximia ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜒 → 𝑦 = 𝑤 ) ) ∧ ∀ 𝑣 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐵 ( 𝜏 ∧ ∀ 𝑤 ∈ 𝐵 ( 𝜃 → 𝑦 = 𝑤 ) ) → 𝑥 = 𝑣 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )
181 15 180 sylbi ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( 𝜂 → ( 𝑏 = 𝑦 ∧ ( 𝜓 → 𝑎 = 𝑥 ) ) ) ) )