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

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ 𝐷 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐷 𝜑 → [ 𝐶 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) ) )