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

Metamath Proof Explorer

Theorem euxfrw

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Version of euxfr with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 14-Nov-2004) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

Ref Expression
Hypotheses euxfrw.1 ⊢ 𝐴 ∈ V
euxfrw.2 ⊢ ∃! 𝑦 𝑥 = 𝐴
euxfrw.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion euxfrw ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 euxfrw.1 ⊢ 𝐴 ∈ V
2 euxfrw.2 ⊢ ∃! 𝑦 𝑥 = 𝐴
3 euxfrw.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4 euex ⊢ ( ∃! 𝑦 𝑥 = 𝐴 → ∃ 𝑦 𝑥 = 𝐴 )
5 2 4 ax-mp ⊢ ∃ 𝑦 𝑥 = 𝐴
6 5 biantrur ⊢ ( 𝜑 ↔ ( ∃ 𝑦 𝑥 = 𝐴 ∧ 𝜑 ) )
7 19.41v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ( ∃ 𝑦 𝑥 = 𝐴 ∧ 𝜑 ) )
8 3 pm5.32i ⊢ ( ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜓 ) )
9 8 exbii ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
10 6 7 9 3bitr2i ⊢ ( 𝜑 ↔ ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
11 10 eubii ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) )
12 2 eumoi ⊢ ∃* 𝑦 𝑥 = 𝐴
13 1 12 euxfr2w ⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 𝜓 )
14 11 13 bitri ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )