Theorem rspsbc2

Description: rspsbc with two quantifying variables. This proof is rspsbc2VD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	rspsbc2	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		idd	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → 𝐶 ∈ 𝐷 ) )
2		rspsbc	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐷 𝜑 ) )
3	2	a1d	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐷 𝜑 ) ) )
4		sbcralg	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐷 𝜑 ↔ ∀ 𝑦 ∈ 𝐷 [ 𝐴 / 𝑥 ] 𝜑 ) )
5	4	biimpd	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑦 ∈ 𝐷 [ 𝐴 / 𝑥 ] 𝜑 ) )
6	3 5	syl6d	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → ∀ 𝑦 ∈ 𝐷 [ 𝐴 / 𝑥 ] 𝜑 ) ) )
7		rspsbc	⊢ ( 𝐶 ∈ 𝐷 → ( ∀ 𝑦 ∈ 𝐷 [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) )
8	1 6 7	syl10	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) ) )