Theorem brralrspcev

Description: Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022)

	Ref	Expression
Assertion	brralrspcev	⊢ ( ( 𝐵 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝑌 𝐴 𝑅 𝐵 ) → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝑅 𝑥 ↔ 𝐴 𝑅 𝐵 ) )
2	1	ralbidv	⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝑌 𝐴 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝐴 𝑅 𝐵 ) )
3	2	rspcev	⊢ ( ( 𝐵 ∈ 𝑋 ∧ ∀ 𝑦 ∈ 𝑌 𝐴 𝑅 𝐵 ) → ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 𝐴 𝑅 𝑥 )