Metamath Proof Explorer

Theorem sbcabel

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

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

Proof

Step Hyp Ref Expression
1 sbcabel.1 ⊢Ⅎ_xB
2 elex ⊢A∈V→A∈V
3 sbcex2 ⊢[˙A/x]˙∃ww=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]˙∀yy∈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↔φ↔∀yy∈w↔[˙A/x]˙φ
11 5 10 bitrid ⊢A∈V→[˙A/x]˙∀yy∈w↔φ↔∀yy∈w↔[˙A/x]˙φ
12 eqabb ⊢w=y|φ↔∀yy∈w↔φ
13 12 sbcbii ⊢[˙A/x]˙w=y|φ↔[˙A/x]˙∀yy∈w↔φ
14 eqabb ⊢w=y|[˙A/x]˙φ↔∀yy∈w↔[˙A/x]˙φ
15 11 13 14 3bitr4g ⊢A∈V→[˙A/x]˙w=y|φ↔w=y|[˙A/x]˙φ
16 1 nfcri ⊢Ⅎxw∈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↔∃ww=y|[˙A/x]˙φ∧w∈B
21 3 20 bitrid ⊢A∈V→[˙A/x]˙∃ww=y|φ∧w∈B↔∃ww=y|[˙A/x]˙φ∧w∈B
22 dfclel ⊢y|φ∈B↔∃ww=y|φ∧w∈B
23 22 sbcbii ⊢[˙A/x]˙y|φ∈B↔[˙A/x]˙∃ww=y|φ∧w∈B
24 dfclel ⊢y|[˙A/x]˙φ∈B↔∃ww=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