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

Theorem cbvrab 3107
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 1707 . . . 4
2 cbvrab.1 . . . . . 6
32nfcri 2612 . . . . 5
4 nfs1v 2181 . . . . 5
53, 4nfan 1928 . . . 4
6 eleq1 2529 . . . . 5
7 sbequ12 1992 . . . . 5
86, 7anbi12d 710 . . . 4
91, 5, 8cbvab 2598 . . 3
10 cbvrab.2 . . . . . 6
1110nfcri 2612 . . . . 5
12 cbvrab.3 . . . . . 6
1312nfsb 2184 . . . . 5
1411, 13nfan 1928 . . . 4
15 nfv 1707 . . . 4
16 eleq1 2529 . . . . 5
17 sbequ 2117 . . . . . 6
18 cbvrab.4 . . . . . . 7
19 cbvrab.5 . . . . . . 7
2018, 19sbie 2149 . . . . . 6
2117, 20syl6bb 261 . . . . 5
2216, 21anbi12d 710 . . . 4
2314, 15, 22cbvab 2598 . . 3
249, 23eqtri 2486 . 2
25 df-rab 2816 . 2
26 df-rab 2816 . 2
2724, 25, 263eqtr4i 2496 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  F/wnf 1616  [wsb 1739  e.wcel 1818  {cab 2442  F/_wnfc 2605  {crab 2811
This theorem is referenced by:  cbvrabv  3108  elrabsf  3366  tfis  6689  cantnflem1  8129  scottexs  8326  scott0s  8327  elmptrab  20328  suppss2f  27477  scottexf  30576  scott0f  30577  eq0rabdioph  30710  rexrabdioph  30727  rexfrabdioph  30728  elnn0rabdioph  30736  dvdsrabdioph  30743  binomcxplemdvsum  31260  stoweidlem34  31816  stoweidlem59  31841  bnj1534  33911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816
  Copyright terms: Public domain W3C validator