Metamath Proof Explorer

Theorem sbcabel

Description: Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005)

Ref Expression
Hypothesis sbcabel.1 ⊢ Ⅎ _ x B
Assertion sbcabel ⊢ A ∈ V → [˙A / x]˙ y | φ ∈ B ↔ y | [˙A / x]˙ φ ∈ B

Proof

Step Hyp Ref Expression
1 sbcabel.1 ⊢ Ⅎ _ x B
2 elex ⊢ A ∈ V → A ∈ V
3 sbcex2 ⊢ [˙A / x]˙ ∃ w w = y | φ ∧ w ∈ B ↔ ∃ w [˙A / x]˙ w = y | φ ∧ w ∈ B
4 sbcan ⊢ [˙A / x]˙ w = y | φ ∧ w ∈ B ↔ [˙A / x]˙ w = y | φ ∧ [˙A / x]˙ w ∈ B
5 sbcal ⊢ [˙A / x]˙ ∀ y y ∈ w ↔ φ ↔ ∀ y [˙A / x]˙ y ∈ w ↔ φ
6 sbcbig ⊢ A ∈ V → [˙A / x]˙ y ∈ w ↔ φ ↔ [˙A / x]˙ y ∈ w ↔ [˙A / x]˙ φ
7 sbcg ⊢ A ∈ V → [˙A / x]˙ y ∈ w ↔ y ∈ w
8 7 bibi1d ⊢ A ∈ V → [˙A / x]˙ y ∈ w ↔ [˙A / x]˙ φ ↔ y ∈ w ↔ [˙A / x]˙ φ
9 6 8 bitrd ⊢ A ∈ V → [˙A / x]˙ y ∈ w ↔ φ ↔ y ∈ w ↔ [˙A / x]˙ φ
10 9 albidv ⊢ A ∈ V → ∀ y [˙A / x]˙ y ∈ w ↔ φ ↔ ∀ y y ∈ w ↔ [˙A / x]˙ φ
11 5 10 bitrid ⊢ A ∈ V → [˙A / x]˙ ∀ y y ∈ w ↔ φ ↔ ∀ y y ∈ w ↔ [˙A / x]˙ φ
12 abeq2 ⊢ w = y | φ ↔ ∀ y y ∈ w ↔ φ
13 12 sbcbii ⊢ [˙A / x]˙ w = y | φ ↔ [˙A / x]˙ ∀ y y ∈ w ↔ φ
14 abeq2 ⊢ w = y | [˙A / x]˙ φ ↔ ∀ y y ∈ w ↔ [˙A / x]˙ φ
15 11 13 14 3bitr4g ⊢ A ∈ V → [˙A / x]˙ w = y | φ ↔ w = y | [˙A / x]˙ φ
16 1 nfcri ⊢ Ⅎ x w ∈ B
17 16 sbcgf ⊢ A ∈ V → [˙A / x]˙ w ∈ B ↔ w ∈ B
18 15 17 anbi12d ⊢ A ∈ V → [˙A / x]˙ w = y | φ ∧ [˙A / x]˙ w ∈ B ↔ w = y | [˙A / x]˙ φ ∧ w ∈ B
19 4 18 bitrid ⊢ A ∈ V → [˙A / x]˙ w = y | φ ∧ w ∈ B ↔ w = y | [˙A / x]˙ φ ∧ w ∈ B
20 19 exbidv ⊢ A ∈ V → ∃ w [˙A / x]˙ w = y | φ ∧ w ∈ B ↔ ∃ w w = y | [˙A / x]˙ φ ∧ w ∈ B
21 3 20 bitrid ⊢ A ∈ V → [˙A / x]˙ ∃ w w = y | φ ∧ w ∈ B ↔ ∃ w w = y | [˙A / x]˙ φ ∧ w ∈ B
22 dfclel ⊢ y | φ ∈ B ↔ ∃ w w = y | φ ∧ w ∈ B
23 22 sbcbii ⊢ [˙A / x]˙ y | φ ∈ B ↔ [˙A / x]˙ ∃ w w = y | φ ∧ w ∈ B
24 dfclel ⊢ y | [˙A / x]˙ φ ∈ B ↔ ∃ w w = y | [˙A / x]˙ φ ∧ w ∈ B
25 21 23 24 3bitr4g ⊢ A ∈ V → [˙A / x]˙ y | φ ∈ B ↔ y | [˙A / x]˙ φ ∈ B
26 2 25 syl ⊢ A ∈ V → [˙A / x]˙ y | φ ∈ B ↔ y | [˙A / x]˙ φ ∈ B