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 ⊢ A ∈ V
euxfrw.2 ⊢ ∃! y x = A
euxfrw.3 ⊢ x = A → φ ↔ ψ
Assertion euxfrw ⊢ ∃! x φ ↔ ∃! y ψ

Proof

Step Hyp Ref Expression
1 euxfrw.1 ⊢ A ∈ V
2 euxfrw.2 ⊢ ∃! y x = A
3 euxfrw.3 ⊢ x = A → φ ↔ ψ
4 euex ⊢ ∃! y x = A → ∃ y x = A
5 2 4 ax-mp ⊢ ∃ y x = A
6 5 biantrur ⊢ φ ↔ ∃ y x = A ∧ φ
7 19.41v ⊢ ∃ y x = A ∧ φ ↔ ∃ y x = A ∧ φ
8 3 pm5.32i ⊢ x = A ∧ φ ↔ x = A ∧ ψ
9 8 exbii ⊢ ∃ y x = A ∧ φ ↔ ∃ y x = A ∧ ψ
10 6 7 9 3bitr2i ⊢ φ ↔ ∃ y x = A ∧ ψ
11 10 eubii ⊢ ∃! x φ ↔ ∃! x ∃ y x = A ∧ ψ
12 2 eumoi ⊢ ∃* y x = A
13 1 12 euxfr2w ⊢ ∃! x ∃ y x = A ∧ ψ ↔ ∃! y ψ
14 11 13 bitri ⊢ ∃! x φ ↔ ∃! y ψ