Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sbcel12gOLD Structured version   Visualization version   Unicode version

Theorem sbcel12gOLD 36905
 Description: Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 18-Aug-2018. Use sbcel12 3772 instead. (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
sbcel12gOLD

Proof of Theorem sbcel12gOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3270 . . 3
2 dfsbcq2 3270 . . . . 5
32abbidv 2569 . . . 4
4 dfsbcq2 3270 . . . . 5
54abbidv 2569 . . . 4
63, 5eleq12d 2523 . . 3
7 nfs1v 2266 . . . . . 6
87nfab 2596 . . . . 5
9 nfs1v 2266 . . . . . 6
109nfab 2596 . . . . 5
118, 10nfel 2604 . . . 4
12 sbab 2578 . . . . 5
13 sbab 2578 . . . . 5
1412, 13eleq12d 2523 . . . 4
1511, 14sbie 2237 . . 3
161, 6, 15vtoclbg 3108 . 2
17 df-csb 3364 . . 3
18 df-csb 3364 . . 3
1917, 18eleq12i 2522 . 2
2016, 19syl6bbr 267 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wceq 1444  wsb 1797   wcel 1887  cab 2437  wsbc 3267  csb 3363 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-sbc 3268  df-csb 3364 This theorem is referenced by:  sbcel2gOLD  36906  csbxpgVD  37291  csbrngVD  37293
 Copyright terms: Public domain W3C validator