New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sbcabel GIF version

Theorem sbcabel 3123
 Description: Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005.)
Hypothesis
Ref Expression
sbcabel.1 xB
Assertion
Ref Expression
sbcabel (A V → ([̣A / x]̣{y φ} B ↔ {y A / xφ} B))
Distinct variable groups:   y,A   x,y
Allowed substitution hints:   φ(x,y)   A(x)   B(x,y)   V(x,y)

Proof of Theorem sbcabel
Dummy variable w is distinct from all other variables.
StepHypRef Expression
1 elex 2867 . 2 (A VA V)
2 sbcexg 3096 . . . 4 (A V → ([̣A / xw(w = {y φ} w B) ↔ wA / x]̣(w = {y φ} w B)))
3 sbcang 3089 . . . . . 6 (A V → ([̣A / x]̣(w = {y φ} w B) ↔ ([̣A / xw = {y φ} A / xw B)))
4 abeq2 2458 . . . . . . . . . 10 (w = {y φ} ↔ y(y wφ))
54sbcbii 3101 . . . . . . . . 9 ([̣A / xw = {y φ} ↔ [̣A / xy(y wφ))
6 sbcalg 3094 . . . . . . . . . 10 (A V → ([̣A / xy(y wφ) ↔ yA / x]̣(y wφ)))
7 sbcbig 3092 . . . . . . . . . . . 12 (A V → ([̣A / x]̣(y wφ) ↔ ([̣A / xy w ↔ [̣A / xφ)))
8 sbcg 3111 . . . . . . . . . . . . 13 (A V → ([̣A / xy wy w))
98bibi1d 310 . . . . . . . . . . . 12 (A V → (([̣A / xy w ↔ [̣A / xφ) ↔ (y w ↔ [̣A / xφ)))
107, 9bitrd 244 . . . . . . . . . . 11 (A V → ([̣A / x]̣(y wφ) ↔ (y w ↔ [̣A / xφ)))
1110albidv 1625 . . . . . . . . . 10 (A V → (yA / x]̣(y wφ) ↔ y(y w ↔ [̣A / xφ)))
126, 11bitrd 244 . . . . . . . . 9 (A V → ([̣A / xy(y wφ) ↔ y(y w ↔ [̣A / xφ)))
135, 12syl5bb 248 . . . . . . . 8 (A V → ([̣A / xw = {y φ} ↔ y(y w ↔ [̣A / xφ)))
14 abeq2 2458 . . . . . . . 8 (w = {y A / xφ} ↔ y(y w ↔ [̣A / xφ))
1513, 14syl6bbr 254 . . . . . . 7 (A V → ([̣A / xw = {y φ} ↔ w = {y A / xφ}))
16 sbcabel.1 . . . . . . . . 9 xB
1716nfcri 2483 . . . . . . . 8 x w B
1817sbcgf 3109 . . . . . . 7 (A V → ([̣A / xw Bw B))
1915, 18anbi12d 691 . . . . . 6 (A V → (([̣A / xw = {y φ} A / xw B) ↔ (w = {y A / xφ} w B)))
203, 19bitrd 244 . . . . 5 (A V → ([̣A / x]̣(w = {y φ} w B) ↔ (w = {y A / xφ} w B)))
2120exbidv 1626 . . . 4 (A V → (wA / x]̣(w = {y φ} w B) ↔ w(w = {y A / xφ} w B)))
222, 21bitrd 244 . . 3 (A V → ([̣A / xw(w = {y φ} w B) ↔ w(w = {y A / xφ} w B)))
23 df-clel 2349 . . . 4 ({y φ} Bw(w = {y φ} w B))
2423sbcbii 3101 . . 3 ([̣A / x]̣{y φ} B ↔ [̣A / xw(w = {y φ} w B))
25 df-clel 2349 . . 3 ({y A / xφ} Bw(w = {y A / xφ} w B))
2622, 24, 253bitr4g 279 . 2 (A V → ([̣A / x]̣{y φ} B ↔ {y A / xφ} B))
271, 26syl 15 1 (A V → ([̣A / x]̣{y φ} B ↔ {y A / xφ} B))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  Ⅎwnfc 2476  Vcvv 2859  [̣wsbc 3046 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-sbc 3047 This theorem is referenced by:  csbexg  3146
 Copyright terms: Public domain W3C validator