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

Theorem cbvralf 2935
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 7-Mar-2004.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
cbvralf.1
cbvralf.2
cbvralf.3
cbvralf.4
cbvralf.5
Assertion
Ref Expression
cbvralf

Proof of Theorem cbvralf
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 nfv 1631 . . . 4
2 cbvralf.1 . . . . . 6
32nfcri 2573 . . . . 5
4 nfs1v 2189 . . . . 5
53, 4nfim 1835 . . . 4
6 eleq1 2503 . . . . 5
7 sbequ12 1948 . . . . 5
86, 7imbi12d 313 . . . 4
91, 5, 8cbval 1986 . . 3
10 cbvralf.2 . . . . . 6
1110nfcri 2573 . . . . 5
12 cbvralf.3 . . . . . 6
1312nfsb 2192 . . . . 5
1411, 13nfim 1835 . . . 4
15 nfv 1631 . . . 4
16 eleq1 2503 . . . . 5
17 sbequ 2116 . . . . . 6
18 cbvralf.4 . . . . . . 7
19 cbvralf.5 . . . . . . 7
2018, 19sbie 2155 . . . . . 6
2117, 20syl6bb 254 . . . . 5
2216, 21imbi12d 313 . . . 4
2314, 15, 22cbval 1986 . . 3
249, 23bitri 242 . 2
25 df-ral 2717 . 2
26 df-ral 2717 . 2
2724, 25, 263bitr4i 270 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  A.wal 1550  F/wnf 1554  [wsb 1660  e.wcel 1728  F/_wnfc 2566  A.wral 2712
This theorem is referenced by:  cbvrexf  2936  cbvral  2937  reusv2lem4  4768  reusv2  4770  ffnfvf  5943  nnwof  10594  scottexf  26865  scott0f  26866  evth2f  27840  evthf  27852  stoweidlem14  27917  stoweidlem28  27931  stoweidlem59  27962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2717
  Copyright terms: Public domain W3C validator