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

Metamath Proof Explorer

Theorem sbcralg

Description: Interchange class substitution and restricted quantifier. (Contributed by NM, 15-Nov-2005) (Proof shortened by Andrew Salmon, 29-Jun-2011)

		Ref	Expression
	Assertion	sbcralg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑦 𝐴
2		sbcralt	⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )