Metamath Proof Explorer


Theorem euxfr2

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 euxfr2w when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses euxfr2.1 𝐴 ∈ V
euxfr2.2 ∃* 𝑦 𝑥 = 𝐴
Assertion euxfr2 ( ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) ↔ ∃! 𝑦 𝜑 )

Proof

Step Hyp Ref Expression
1 euxfr2.1 𝐴 ∈ V
2 euxfr2.2 ∃* 𝑦 𝑥 = 𝐴
3 2euswap ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 = 𝐴𝜑 ) → ( ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) → ∃! 𝑦𝑥 ( 𝑥 = 𝐴𝜑 ) ) )
4 2 moani ∃* 𝑦 ( 𝜑𝑥 = 𝐴 )
5 ancom ( ( 𝜑𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴𝜑 ) )
6 5 mobii ( ∃* 𝑦 ( 𝜑𝑥 = 𝐴 ) ↔ ∃* 𝑦 ( 𝑥 = 𝐴𝜑 ) )
7 4 6 mpbi ∃* 𝑦 ( 𝑥 = 𝐴𝜑 )
8 3 7 mpg ( ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) → ∃! 𝑦𝑥 ( 𝑥 = 𝐴𝜑 ) )
9 2euswap ( ∀ 𝑦 ∃* 𝑥 ( 𝑥 = 𝐴𝜑 ) → ( ∃! 𝑦𝑥 ( 𝑥 = 𝐴𝜑 ) → ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) ) )
10 moeq ∃* 𝑥 𝑥 = 𝐴
11 10 moani ∃* 𝑥 ( 𝜑𝑥 = 𝐴 )
12 5 mobii ( ∃* 𝑥 ( 𝜑𝑥 = 𝐴 ) ↔ ∃* 𝑥 ( 𝑥 = 𝐴𝜑 ) )
13 11 12 mpbi ∃* 𝑥 ( 𝑥 = 𝐴𝜑 )
14 9 13 mpg ( ∃! 𝑦𝑥 ( 𝑥 = 𝐴𝜑 ) → ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) )
15 8 14 impbii ( ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) ↔ ∃! 𝑦𝑥 ( 𝑥 = 𝐴𝜑 ) )
16 biidd ( 𝑥 = 𝐴 → ( 𝜑𝜑 ) )
17 1 16 ceqsexv ( ∃ 𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ 𝜑 )
18 17 eubii ( ∃! 𝑦𝑥 ( 𝑥 = 𝐴𝜑 ) ↔ ∃! 𝑦 𝜑 )
19 15 18 bitri ( ∃! 𝑥𝑦 ( 𝑥 = 𝐴𝜑 ) ↔ ∃! 𝑦 𝜑 )