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

Theorem cbvrab 2871
 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 1624 . . . 4
2 cbvrab.1 . . . . . 6
32nfcri 2496 . . . . 5
4 nfs1v 2119 . . . . 5
53, 4nfan 1834 . . . 4
6 eleq1 2426 . . . . 5
7 sbequ12 1931 . . . . 5
86, 7anbi12d 691 . . . 4
91, 5, 8cbvab 2484 . . 3
10 cbvrab.2 . . . . . 6
1110nfcri 2496 . . . . 5
12 cbvrab.3 . . . . . 6
1312nfsb 2122 . . . . 5
1411, 13nfan 1834 . . . 4
15 nfv 1624 . . . 4
16 eleq1 2426 . . . . 5
17 sbequ 2073 . . . . . 6
18 cbvrab.4 . . . . . . 7
19 cbvrab.5 . . . . . . 7
2018, 19sbie 2051 . . . . . 6
2117, 20syl6bb 252 . . . . 5
2216, 21anbi12d 691 . . . 4
2314, 15, 22cbvab 2484 . . 3
249, 23eqtri 2386 . 2
25 df-rab 2637 . 2
26 df-rab 2637 . 2
2724, 25, 263eqtr4i 2396 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wnf 1549   wceq 1647  wsb 1653   wcel 1715  cab 2352  wnfc 2489  crab 2632 This theorem is referenced by:  cbvrabv  2872  elrabsf  3115  tfis  4748  scottexs  7704  scott0s  7705  elmptrab  17735  suppss2f  23452  ustuqtop  23749  ballotlemelo  24193  ballotleme  24202  itgaddnclem2  25682  eq0rabdioph  26362  rexrabdioph  26381  rexfrabdioph  26382  elnn0rabdioph  26390  dvdsrabdioph  26397  stoweidlem34  27289  stoweidlem49  27304  stoweidlem59  27314  bnj1534  28649 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637
 Copyright terms: Public domain W3C validator