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 ⊢ 𝐴 ∈ V
euxfr.2 ⊢ ∃! 𝑦 𝑥 = 𝐴
euxfr.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion euxfr ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 euxfr.1 ⊢ 𝐴 ∈ V
2 euxfr.2 ⊢ ∃! 𝑦 𝑥 = 𝐴
3 euxfr.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 euxfr2 ⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃! 𝑦 𝜓 )
14 11 13 bitri ⊢ ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )