This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reuxfrd

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . (Contributed by NM, 16-Jan-2012) Separate variables B and C . (Revised by Thierry Arnoux, 8-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 reuxfrd.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
2 reuxfrd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
3 rmoan ⊢ ( ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃* 𝑦 ∈ 𝐶 ( 𝜓 ∧ 𝑥 = 𝐴 ) )
4 2 3 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 ( 𝜓 ∧ 𝑥 = 𝐴 ) )
5 ancom ⊢ ( ( 𝜓 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜓 ) )
6 5 rmobii ⊢ ( ∃* 𝑦 ∈ 𝐶 ( 𝜓 ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
7 4 6 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
8 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
9 2reuswap ⊢ ( ∀ 𝑥 ∈ 𝐵 ∃* 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
10 8 9 syl ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
11 2reuswap2 ⊢ ( ∀ 𝑦 ∈ 𝐶 ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) → ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
12 moeq ⊢ ∃* 𝑥 𝑥 = 𝐴
13 12 moani ⊢ ∃* 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 )
14 ancom ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
15 an12 ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
16 14 15 bitri ⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
17 16 mobii ⊢ ( ∃* 𝑥 ( ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
18 13 17 mpbi ⊢ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) )
19 18 a1i ⊢ ( 𝑦 ∈ 𝐶 → ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
20 11 19 mprg ⊢ ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) → ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
21 10 20 impbid1 ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
22 biidd ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜓 ) )
23 22 ceqsrexv ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ 𝜓 ) )
24 1 23 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ 𝜓 ) )
25 24 reubidva ⊢ ( 𝜑 → ( ∃! 𝑦 ∈ 𝐶 ∃ 𝑥 ∈ 𝐵 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) )
26 21 25 bitrd ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜓 ) )