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

Theorem cbvrab 3042
 Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
cbvrab.1
cbvrab.2
cbvrab.3
cbvrab.4
cbvrab.5
Assertion
Ref Expression
cbvrab

Proof of Theorem cbvrab
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfv 1760 . . . 4
2 cbvrab.1 . . . . . 6
32nfcri 2585 . . . . 5
4 nfs1v 2265 . . . . 5
53, 4nfan 2010 . . . 4
6 eleq1 2516 . . . . 5
7 sbequ12 2082 . . . . 5
86, 7anbi12d 716 . . . 4
91, 5, 8cbvab 2573 . . 3
10 cbvrab.2 . . . . . 6
1110nfcri 2585 . . . . 5
12 cbvrab.3 . . . . . 6
1312nfsb 2268 . . . . 5
1411, 13nfan 2010 . . . 4
15 nfv 1760 . . . 4
16 eleq1 2516 . . . . 5
17 sbequ 2204 . . . . . 6
18 cbvrab.4 . . . . . . 7
19 cbvrab.5 . . . . . . 7
2018, 19sbie 2236 . . . . . 6
2117, 20syl6bb 265 . . . . 5
2216, 21anbi12d 716 . . . 4
2314, 15, 22cbvab 2573 . . 3
249, 23eqtri 2472 . 2
25 df-rab 2745 . 2
26 df-rab 2745 . 2
2724, 25, 263eqtr4i 2482 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1443  wnf 1666  wsb 1796   wcel 1886  cab 2436  wnfc 2578  crab 2740 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745 This theorem is referenced by:  cbvrabv  3043  elrabsf  3305  tfis  6678  cantnflem1  8191  scottexs  8355  scott0s  8356  elmptrab  20835  suppss2fOLD  28230  bnj1534  29657  scottexf  32404  scott0f  32405  eq0rabdioph  35613  rexrabdioph  35631  rexfrabdioph  35632  elnn0rabdioph  35640  dvdsrabdioph  35647  binomcxplemdvsum  36698  stoweidlem34  37889  stoweidlem59  37914
 Copyright terms: Public domain W3C validator