Theorem rexlimdvaacbv

Description: Unpack a restricted existential antecedent while changing the variable with implicit substitution. The equivalent of this theorem without the bound variable change is rexlimdvaa . (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	rexlimdvaacbv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
	rexlimdvaacbv.2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜃 ) ) → 𝜒 )
Assertion	rexlimdvaacbv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		rexlimdvaacbv.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
2		rexlimdvaacbv.2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝜃 ) ) → 𝜒 )
3	1	cbvrexv	⊢ ( ∃ 𝑥 ∈ 𝐴 𝜓 ↔ ∃ 𝑦 ∈ 𝐴 𝜃 )
4	2	rexlimdvaa	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐴 𝜃 → 𝜒 ) )
5	3 4	biimtrid	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝜓 → 𝜒 ) )