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

Theorem cbvral 3080
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)
Hypotheses
Ref Expression
cbvral.1
cbvral.2
cbvral.3
Assertion
Ref Expression
cbvral
Distinct variable groups:   ,   ,

Proof of Theorem cbvral
StepHypRef Expression
1 nfcv 2619 . 2
2 nfcv 2619 . 2
3 cbvral.1 . 2
4 cbvral.2 . 2
5 cbvral.3 . 2
61, 2, 3, 4, 5cbvralf 3078 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  F/wnf 1616  A.wral 2807
This theorem is referenced by:  cbvralv  3084  cbvralsv  3095  cbviin  4368  disjxun  4450  ralxpf  5154  eqfnfv2f  5985  ralrnmpt  6040  dff13f  6167  ofrfval2  6557  fmpt2x  6866  ovmptss  6881  cbvixp  7506  mptelixpg  7526  boxcutc  7532  xpf1o  7699  indexfi  7848  ixpiunwdom  8038  dfac8clem  8434  acni2  8448  ac6num  8880  ac6c4  8882  iundom2g  8936  uniimadomf  8941  rabssnn0fi  12095  rlim2  13319  ello1mpt  13344  o1compt  13410  fsum00  13612  iserodd  14359  pcmptdvds  14413  catpropd  15104  invfuc  15343  gsummptnn0fz  17014  dprdwdOLD2  17045  dprdwdOLD  17051  gsummoncoe1  18346  gsumply1eq  18347  fiuncmp  19904  elptr2  20075  ptcld  20114  ptclsg  20116  ptcnplem  20122  cnmpt11  20164  cnmpt21  20172  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  finiunmbl  21954  volfiniun  21957  iunmbl  21963  voliun  21964  mbfeqalem  22049  mbfsup  22071  mbfinf  22072  mbflim  22075  itg2split  22156  itgeqa  22220  itgfsum  22233  itgabs  22241  itggt0  22248  limciun  22298  dvlipcn  22395  dvfsumlem4  22430  dvfsum2  22435  itgsubst  22450  coeeq2  22639  ulmss  22792  leibpi  23273  rlimcnp  23295  o1cxp  23304  fsumdvdscom  23461  lgseisenlem2  23625  disjunsn  27453  lgamgulmlem6  28576  itgabsnc  30084  itggt0cn  30087  totbndbnd  30285  climinff  31617  idlimc  31632  cncfshift  31676  stoweidlem31  31813  cbvral2  32177  bnj110  33916  bnj1529  34126
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