Metamath Proof Explorer


Theorem moxfr

Description: Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015)

Ref Expression
Hypotheses moxfr.a 𝐴 ∈ V
moxfr.b ∃! 𝑦 𝑥 = 𝐴
moxfr.c ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
Assertion moxfr ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )

Proof

Step Hyp Ref Expression
1 moxfr.a 𝐴 ∈ V
2 moxfr.b ∃! 𝑦 𝑥 = 𝐴
3 moxfr.c ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) )
4 1 a1i ( 𝑦 ∈ V → 𝐴 ∈ V )
5 euex ( ∃! 𝑦 𝑥 = 𝐴 → ∃ 𝑦 𝑥 = 𝐴 )
6 2 5 ax-mp 𝑦 𝑥 = 𝐴
7 rexv ( ∃ 𝑦 ∈ V 𝑥 = 𝐴 ↔ ∃ 𝑦 𝑥 = 𝐴 )
8 6 7 mpbir 𝑦 ∈ V 𝑥 = 𝐴
9 8 a1i ( 𝑥 ∈ V → ∃ 𝑦 ∈ V 𝑥 = 𝐴 )
10 4 9 3 rexxfr ( ∃ 𝑥 ∈ V 𝜑 ↔ ∃ 𝑦 ∈ V 𝜓 )
11 rexv ( ∃ 𝑥 ∈ V 𝜑 ↔ ∃ 𝑥 𝜑 )
12 rexv ( ∃ 𝑦 ∈ V 𝜓 ↔ ∃ 𝑦 𝜓 )
13 10 11 12 3bitr3i ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 𝜓 )
14 1 2 3 euxfrw ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 𝜓 )
15 13 14 imbi12i ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 𝜓 → ∃! 𝑦 𝜓 ) )
16 moeu ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
17 moeu ( ∃* 𝑦 𝜓 ↔ ( ∃ 𝑦 𝜓 → ∃! 𝑦 𝜓 ) )
18 15 16 17 3bitr4i ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )