Metamath Proof Explorer

Theorem sbcralt

Description: Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008) (Revised by David Abernethy, 22-Feb-2010)

Ref Expression
Assertion sbcralt ⊢ A ∈ V ∧ Ⅎ _ y A → [˙A / x]˙ ∀ y ∈ B φ ↔ ∀ y ∈ B [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbccow ⊢ [˙A / z]˙ [˙z / x]˙ ∀ y ∈ B φ ↔ [˙A / x]˙ ∀ y ∈ B φ
2 simpl ⊢ A ∈ V ∧ Ⅎ _ y A → A ∈ V
3 sbsbc ⊢ z x ∀ y ∈ B φ ↔ [˙z / x]˙ ∀ y ∈ B φ
4 nfcv ⊢ Ⅎ _ x B
5 nfs1v ⊢ Ⅎ x z x φ
6 4 5 nfralw ⊢ Ⅎ x ∀ y ∈ B z x φ
7 sbequ12 ⊢ x = z → φ ↔ z x φ
8 7 ralbidv ⊢ x = z → ∀ y ∈ B φ ↔ ∀ y ∈ B z x φ
9 6 8 sbiev ⊢ z x ∀ y ∈ B φ ↔ ∀ y ∈ B z x φ
10 3 9 bitr3i ⊢ [˙z / x]˙ ∀ y ∈ B φ ↔ ∀ y ∈ B z x φ
11 nfnfc1 ⊢ Ⅎ y Ⅎ _ y A
12 nfcvd ⊢ Ⅎ _ y A → Ⅎ _ y z
13 id ⊢ Ⅎ _ y A → Ⅎ _ y A
14 12 13 nfeqd ⊢ Ⅎ _ y A → Ⅎ y z = A
15 11 14 nfan1 ⊢ Ⅎ y Ⅎ _ y A ∧ z = A
16 dfsbcq2 ⊢ z = A → z x φ ↔ [˙A / x]˙ φ
17 16 adantl ⊢ Ⅎ _ y A ∧ z = A → z x φ ↔ [˙A / x]˙ φ
18 15 17 ralbid ⊢ Ⅎ _ y A ∧ z = A → ∀ y ∈ B z x φ ↔ ∀ y ∈ B [˙A / x]˙ φ
19 18 adantll ⊢ A ∈ V ∧ Ⅎ _ y A ∧ z = A → ∀ y ∈ B z x φ ↔ ∀ y ∈ B [˙A / x]˙ φ
20 10 19 bitrid ⊢ A ∈ V ∧ Ⅎ _ y A ∧ z = A → [˙z / x]˙ ∀ y ∈ B φ ↔ ∀ y ∈ B [˙A / x]˙ φ
21 2 20 sbcied ⊢ A ∈ V ∧ Ⅎ _ y A → [˙A / z]˙ [˙z / x]˙ ∀ y ∈ B φ ↔ ∀ y ∈ B [˙A / x]˙ φ
22 1 21 bitr3id ⊢ A ∈ V ∧ Ⅎ _ y A → [˙A / x]˙ ∀ y ∈ B φ ↔ ∀ y ∈ B [˙A / x]˙ φ