Theorem rmoeqd

Description: Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Hypothesis	raleqd.1	⊢ ( 𝐴 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rmoeqd	⊢ ( 𝐴 = 𝐵 → ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		raleqd.1	⊢ ( 𝐴 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
2		rmoeq1	⊢ ( 𝐴 = 𝐵 → ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ∈ 𝐵 𝜑 ) )
3	1	rmobidv	⊢ ( 𝐴 = 𝐵 → ( ∃* 𝑥 ∈ 𝐵 𝜑 ↔ ∃* 𝑥 ∈ 𝐵 𝜓 ) )
4	2 3	bitrd	⊢ ( 𝐴 = 𝐵 → ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ∈ 𝐵 𝜓 ) )