Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcel12 Structured version   Unicode version

Theorem sbcel12 3828
 Description: Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005.) (Revised by NM, 18-Aug-2018.)
Assertion
Ref Expression
sbcel12

Proof of Theorem sbcel12
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3339 . . . 4
2 dfsbcq2 3339 . . . . . 6
32abbidv 2603 . . . . 5
4 dfsbcq2 3339 . . . . . 6
54abbidv 2603 . . . . 5
63, 5eleq12d 2549 . . . 4
7 nfs1v 2164 . . . . . . 7
87nfab 2633 . . . . . 6
9 nfs1v 2164 . . . . . . 7
109nfab 2633 . . . . . 6
118, 10nfel 2642 . . . . 5
12 sbab 2614 . . . . . 6
13 sbab 2614 . . . . . 6
1412, 13eleq12d 2549 . . . . 5
1511, 14sbie 2123 . . . 4
161, 6, 15vtoclbg 3177 . . 3
17 df-csb 3441 . . . 4
18 df-csb 3441 . . . 4
1917, 18eleq12i 2546 . . 3
2016, 19syl6bbr 263 . 2
21 sbcex 3346 . . . 4
2221con3i 135 . . 3
23 noel 3794 . . . 4
24 csbprc 3826 . . . . . 6
2524eleq2d 2537 . . . . 5
2625notbid 294 . . . 4
2723, 26mpbiri 233 . . 3
2822, 272falsed 351 . 2
2920, 28pm2.61i 164 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 184   wceq 1379  wsb 1711   wcel 1767  cab 2452  cvv 3118  wsbc 3336  csb 3440  c0 3790 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-in 3488  df-ss 3495  df-nul 3791 This theorem is referenced by:  sbcnel12g  3831  sbcel1g  3834  sbcel2  3836  sbccsb2  3856  csbmpt12  4787  ixpsnval  7484  fmptdF  27318  finixpnum  29965
 Copyright terms: Public domain W3C validator