Metamath Proof Explorer

Theorem reuxfrdf

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfrd (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017) (Revised by Thierry Arnoux, 30-Mar-2018)

Ref Expression
Hypotheses reuxfrdf.0 ⊢ Ⅎ 𝑦 𝐵
reuxfrdf.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
reuxfrdf.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
Assertion reuxfrdf ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) )

Proof

Step Hyp Ref Expression
1 reuxfrdf.0 ⊢ Ⅎ 𝑦 𝐵
2 reuxfrdf.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
3 reuxfrdf.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
4 rmoan ⊢ ( ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃* 𝑦 ∈ 𝐶 ( 𝜓 ∧ 𝑥 = 𝐴 ) )
5 3 4 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 ( 𝜓 ∧ 𝑥 = 𝐴 ) )
6 ancom ⊢ ( ( 𝜓 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜓 ) )
7 6 rmobii ⊢ ( ∃* 𝑦 ∈ 𝐶 ( 𝜓 ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
8 5 7 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
9 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
10 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
11 10 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
12 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
13 1 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐵
14 13 moanim ⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ( 𝑥 ∈ 𝐵 → ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
15 14 albii ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
16 12 15 bitr4i ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
17 2euswapv ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) → ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) → ∃! 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ) )
18 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
19 13 r19.41 ⊢ ( ∃ 𝑦 ∈ 𝐶 ( ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐵 ) ↔ ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐵 ) )
20 ancom ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐵 ) )
21 20 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ∈ 𝐶 ( ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐵 ) )
22 ancom ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐵 ) )
23 19 21 22 3bitr4i ⊢ ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
24 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
25 23 24 bitr3i ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
26 an12 ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
27 26 exbii ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
28 25 27 bitri ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
29 28 eubii ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
30 18 29 bitri ⊢ ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
31 df-reu ⊢ ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
32 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐶
33 32 r19.41 ⊢ ( ∃ 𝑥 ∈ 𝐵 ( ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑦 ∈ 𝐶 ) ↔ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑦 ∈ 𝐶 ) )
34 ancom ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑦 ∈ 𝐶 ) )
35 34 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑦 ∈ 𝐶 ) )
36 ancom ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ∧ 𝑦 ∈ 𝐶 ) )
37 33 35 36 3bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
38 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
39 37 38 bitr3i ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
40 39 eubii ⊢ ( ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
41 31 40 bitri ⊢ ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
42 17 30 41 3imtr4g ⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
43 16 42 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
44 11 43 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
45 9 44 syl ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
46 df-ral ⊢ ( ∀ 𝑦 ∈ 𝐶 ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
47 moanimv ⊢ ( ∃* 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ( 𝑦 ∈ 𝐶 → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
48 47 albii ⊢ ( ∀ 𝑦 ∃* 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐶 → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
49 46 48 bitr4i ⊢ ( ∀ 𝑦 ∈ 𝐶 ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
50 2euswapv ⊢ ( ∀ 𝑦 ∃* 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) → ( ∃! 𝑦 ∃ 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) → ∃! 𝑥 ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ) )
51 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
52 51 38 bitr3i ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
53 an12 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
54 53 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
55 52 54 bitri ⊢ ( ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
56 55 eubii ⊢ ( ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
57 31 56 bitri ⊢ ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
58 25 eubii ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
59 18 58 bitri ⊢ ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) )
60 50 57 59 3imtr4g ⊢ ( ∀ 𝑦 ∃* 𝑥 ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ) → ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
61 49 60 sylbi ⊢ ( ∀ 𝑦 ∈ 𝐶 ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) → ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
62 moeq ⊢ ∃* 𝑥 𝑥 = 𝐴
63 62 moani ⊢ ∃* 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 )
64 ancom ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
65 an12 ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
66 64 65 bitri ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
67 66 mobii ⊢ ( ∃* 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
68 63 67 mpbi ⊢ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) )
69 68 a1i ⊢ ( 𝑦 ∈ 𝐶 → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
70 61 69 mprg ⊢ ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
71 45 70 impbid1 ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
72 biidd ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜓 ) )
73 72 ceqsrexv ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ 𝜓 ) )
74 2 73 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ 𝜓 ) )
75 74 reubidva ⊢ ( 𝜑 → ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) )
76 71 75 bitrd ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) )