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

Theorem cbvralf 3078
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 1707 . . . 4
2 cbvralf.1 . . . . . 6
32nfcri 2612 . . . . 5
4 nfs1v 2181 . . . . 5
53, 4nfim 1920 . . . 4
6 eleq1 2529 . . . . 5
7 sbequ12 1992 . . . . 5
86, 7imbi12d 320 . . . 4
91, 5, 8cbval 2021 . . 3
10 cbvralf.2 . . . . . 6
1110nfcri 2612 . . . . 5
12 cbvralf.3 . . . . . 6
1312nfsb 2184 . . . . 5
1411, 13nfim 1920 . . . 4
15 nfv 1707 . . . 4
16 eleq1 2529 . . . . 5
17 sbequ 2117 . . . . . 6
18 cbvralf.4 . . . . . . 7
19 cbvralf.5 . . . . . . 7
2018, 19sbie 2149 . . . . . 6
2117, 20syl6bb 261 . . . . 5
2216, 21imbi12d 320 . . . 4
2314, 15, 22cbval 2021 . . 3
249, 23bitri 249 . 2
25 df-ral 2812 . 2
26 df-ral 2812 . 2
2724, 25, 263bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616  [wsb 1739  e.wcel 1818  F/_wnfc 2605  A.wral 2807
This theorem is referenced by:  cbvrexf  3079  cbvral  3080  reusv2lem4  4656  reusv2  4658  ffnfvf  6058  nnwof  11177  nnindf  27610  scottexf  30576  scott0f  30577  evth2f  31390  evthf  31402  stoweidlem14  31796  stoweidlem28  31810  stoweidlem59  31841
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-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
  Copyright terms: Public domain W3C validator