Theorem rexeqtrdv

Description: Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025)

	Ref	Expression
Hypotheses	rexeqtrdv.1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
	rexeqtrdv.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	rexeqtrdv	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		rexeqtrdv.1	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 )
2		rexeqtrdv.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	2	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑥 ∈ 𝐵 𝜓 ) )
4	1 3	mpbid	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )