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

Metamath Proof Explorer

Theorem euxfr

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker euxfrw when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses euxfr.1 ⊢ A ∈ V
euxfr.2 ⊢ ∃! y x = A
euxfr.3 ⊢ x = A → φ ↔ ψ
Assertion euxfr ⊢ ∃! x φ ↔ ∃! y ψ

Proof

Step Hyp Ref Expression
1 euxfr.1 ⊢ A ∈ V
2 euxfr.2 ⊢ ∃! y x = A
3 euxfr.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 euxfr2 ⊢ ∃! x ∃ y x = A ∧ ψ ↔ ∃! y ψ
14 11 13 bitri ⊢ ∃! x φ ↔ ∃! y ψ