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	⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 𝜓 )