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 ⊢ A ∈ B → C ∈ D → ∀ x ∈ B ∀ y ∈ D φ → [˙C / y]˙ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 idd ⊢ A ∈ B → C ∈ D → C ∈ D
2 rspsbc ⊢ A ∈ B → ∀ x ∈ B ∀ y ∈ D φ → [˙A / x]˙ ∀ y ∈ D φ
3 2 a1d ⊢ A ∈ B → C ∈ D → ∀ x ∈ B ∀ y ∈ D φ → [˙A / x]˙ ∀ y ∈ D φ
4 sbcralg ⊢ A ∈ B → [˙A / x]˙ ∀ y ∈ D φ ↔ ∀ y ∈ D [˙A / x]˙ φ
5 4 biimpd ⊢ A ∈ B → [˙A / x]˙ ∀ y ∈ D φ → ∀ y ∈ D [˙A / x]˙ φ
6 3 5 syl6d ⊢ A ∈ B → C ∈ D → ∀ x ∈ B ∀ y ∈ D φ → ∀ y ∈ D [˙A / x]˙ φ
7 rspsbc ⊢ C ∈ D → ∀ y ∈ D [˙A / x]˙ φ → [˙C / y]˙ [˙A / x]˙ φ
8 1 6 7 syl10 ⊢ A ∈ B → C ∈ D → ∀ x ∈ B ∀ y ∈ D φ → [˙C / y]˙ [˙A / x]˙ φ