Metamath Proof Explorer

Theorem 2reuimp0

Description: Implication of a double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification. The involved wffs depend on the setvar variables as follows: ph(a,b), th(a,c), ch(d,b), ta(d,c), et(a,e), ps(a,f) (Contributed by AV, 13-Mar-2023)

Ref Expression
Hypotheses 2reuimp.c ⊢ ( 𝑏 = 𝑐 → ( 𝜑 ↔ 𝜃 ) )
2reuimp.d ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜒 ) )
2reuimp.a ⊢ ( 𝑎 = 𝑑 → ( 𝜃 ↔ 𝜏 ) )
2reuimp.e ⊢ ( 𝑏 = 𝑒 → ( 𝜑 ↔ 𝜂 ) )
2reuimp.f ⊢ ( 𝑐 = 𝑓 → ( 𝜃 ↔ 𝜓 ) )
Assertion 2reuimp0 ( ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 2reuimp.c ⊢ ( 𝑏 = 𝑐 → ( 𝜑 ↔ 𝜃 ) )
2 2reuimp.d ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜒 ) )
3 2reuimp.a ⊢ ( 𝑎 = 𝑑 → ( 𝜃 ↔ 𝜏 ) )
4 2reuimp.e ⊢ ( 𝑏 = 𝑒 → ( 𝜑 ↔ 𝜂 ) )
5 2reuimp.f ⊢ ( 𝑐 = 𝑓 → ( 𝜃 ↔ 𝜓 ) )
6 1 reu8 ⊢ ( ∃! 𝑏 ∈ 𝑉 𝜑 ↔ ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) )
7 6 reubii ⊢ ( ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 ↔ ∃! 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) )
8 3 imbi1d ⊢ ( 𝑎 = 𝑑 → ( ( 𝜃 → 𝑏 = 𝑐 ) ↔ ( 𝜏 → 𝑏 = 𝑐 ) ) )
9 8 ralbidv ⊢ ( 𝑎 = 𝑑 → ( ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ↔ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) )
10 2 9 anbi12d ⊢ ( 𝑎 = 𝑑 → ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ↔ ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) ) )
11 10 rexbidv ⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ↔ ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) ) )
12 11 reu8 ⊢ ( ∃! 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ↔ ∃ 𝑎 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ∀ 𝑑 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) )
13 r19.28v ⊢ ( ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ∀ 𝑑 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑑 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) )
14 equequ1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 = 𝑐 ↔ 𝑒 = 𝑐 ) )
15 14 imbi2d ⊢ ( 𝑏 = 𝑒 → ( ( 𝜃 → 𝑏 = 𝑐 ) ↔ ( 𝜃 → 𝑒 = 𝑐 ) ) )
16 15 ralbidv ⊢ ( 𝑏 = 𝑒 → ( ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ↔ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) )
17 4 16 anbi12d ⊢ ( 𝑏 = 𝑒 → ( ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ↔ ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) )
18 17 cbvrexvw ⊢ ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ↔ ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) )
19 r19.23v ⊢ ( ∀ 𝑏 ∈ 𝑉 ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ↔ ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) )
20 r19.28v ⊢ ( ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ∀ 𝑏 ∈ 𝑉 ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑏 ∈ 𝑉 ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) )
21 ancom ⊢ ( ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ↔ ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ∧ ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) )
22 r19.42v ⊢ ( ∃ 𝑒 ∈ 𝑉 ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ∧ ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) ↔ ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ∧ ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) )
23 21 22 bitr4i ⊢ ( ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ↔ ∃ 𝑒 ∈ 𝑉 ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ∧ ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) )
24 equequ2 ⊢ ( 𝑐 = 𝑓 → ( 𝑒 = 𝑐 ↔ 𝑒 = 𝑓 ) )
25 5 24 imbi12d ⊢ ( 𝑐 = 𝑓 → ( ( 𝜃 → 𝑒 = 𝑐 ) ↔ ( 𝜓 → 𝑒 = 𝑓 ) ) )
26 25 cbvralvw ⊢ ( ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ↔ ∀ 𝑓 ∈ 𝑉 ( 𝜓 → 𝑒 = 𝑓 ) )
27 r19.28v ⊢ ( ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ∀ 𝑓 ∈ 𝑉 ( 𝜓 → 𝑒 = 𝑓 ) ) → ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
28 27 ex ⊢ ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ( ∀ 𝑓 ∈ 𝑉 ( 𝜓 → 𝑒 = 𝑓 ) → ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ) )
29 28 expcom ⊢ ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( 𝜂 → ( ∀ 𝑓 ∈ 𝑉 ( 𝜓 → 𝑒 = 𝑓 ) → ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ) ) )
30 26 29 syl7bi ⊢ ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ( 𝜂 → ( ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) → ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ) ) )
31 30 imp32 ⊢ ( ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ∧ ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) → ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
32 31 reximi ⊢ ( ∃ 𝑒 ∈ 𝑉 ( ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ∧ ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ) → ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
33 23 32 sylbi ⊢ ( ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
34 33 ralimi ⊢ ( ∀ 𝑏 ∈ 𝑉 ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
35 20 34 syl ⊢ ( ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) ∧ ∀ 𝑏 ∈ 𝑉 ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
36 35 ex ⊢ ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) → ( ∀ 𝑏 ∈ 𝑉 ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ) )
37 19 36 syl5bir ⊢ ( ∃ 𝑒 ∈ 𝑉 ( 𝜂 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑒 = 𝑐 ) ) → ( ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ) )
38 18 37 sylbi ⊢ ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) → ( ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) ) )
39 38 imp ⊢ ( ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
40 39 ralimi ⊢ ( ∀ 𝑑 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
41 13 40 syl ⊢ ( ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ∀ 𝑑 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
42 41 reximi ⊢ ( ∃ 𝑎 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) ∧ ∀ 𝑑 ∈ 𝑉 ( ∃ 𝑏 ∈ 𝑉 ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
43 12 42 sylbi ⊢ ( ∃! 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝜑 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜃 → 𝑏 = 𝑐 ) ) → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )
44 7 43 sylbi ⊢ ( ∃! 𝑎 ∈ 𝑉 ∃! 𝑏 ∈ 𝑉 𝜑 → ∃ 𝑎 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ∃ 𝑒 ∈ 𝑉 ∀ 𝑓 ∈ 𝑉 ( ( 𝜂 ∧ ( ( 𝜒 ∧ ∀ 𝑐 ∈ 𝑉 ( 𝜏 → 𝑏 = 𝑐 ) ) → 𝑎 = 𝑑 ) ) ∧ ( 𝜓 → 𝑒 = 𝑓 ) ) )