Theorem rexeqtrrdv

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

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

Proof

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