This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brimralrspcev

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

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

Proof

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