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

Theorem cbvral 3084
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)
Hypotheses
Ref Expression
cbvral.1  |-  F/ y
ph
cbvral.2  |-  F/ x ps
cbvral.3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvral  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Distinct variable groups:    x, A    y, A
Allowed substitution hints:    ph( x, y)    ps( x, y)

Proof of Theorem cbvral
StepHypRef Expression
1 nfcv 2629 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ y A
3 cbvral.1 . 2  |-  F/ y
ph
4 cbvral.2 . 2  |-  F/ x ps
5 cbvral.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvralf 3082 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1599   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  cbvralv  3088  cbvralsv  3099  cbviin  4363  disjxun  4445  ralxpf  5149  eqfnfv2f  5979  ralrnmpt  6030  dff13f  6155  ofrfval2  6541  fmpt2x  6850  ovmptss  6864  cbvixp  7486  mptelixpg  7506  boxcutc  7512  xpf1o  7679  indexfi  7828  ixpiunwdom  8017  dfac8clem  8413  acni2  8427  ac6num  8859  ac6c4  8861  iundom2g  8915  uniimadomf  8920  rabssnn0fi  12063  rlim2  13282  ello1mpt  13307  o1compt  13373  fsum00  13575  iserodd  14218  pcmptdvds  14272  catpropd  14965  invfuc  15201  gsummptnn0fz  16817  dprdwd  16847  dprdwdOLD  16853  gsummoncoe1  18145  gsumply1eq  18146  fiuncmp  19698  elptr2  19838  ptcld  19877  ptclsg  19879  ptcnplem  19885  cnmpt11  19927  cnmpt21  19935  ovoliunlem3  21678  ovoliun  21679  ovoliun2  21680  finiunmbl  21717  volfiniun  21720  iunmbl  21726  voliun  21727  mbfeqalem  21812  mbfsup  21834  mbfinf  21835  mbflim  21838  itg2split  21919  itgeqa  21983  itgfsum  21996  itgabs  22004  itggt0  22011  limciun  22061  dvlipcn  22158  dvfsumlem4  22193  dvfsum2  22198  itgsubst  22213  coeeq2  22402  ulmss  22554  leibpi  23029  rlimcnp  23051  o1cxp  23060  fsumdvdscom  23217  lgseisenlem2  23381  disjunsn  27154  nn0min  27307  voliune  27869  volfiniune  27870  lgamgulmlem6  28244  itgabsnc  29689  itggt0cn  29692  totbndbnd  29916  climinff  31181  idlimc  31196  cncfshift  31240  stoweidlem31  31359  fourierdlem68  31503  fourierdlem73  31508  fourierdlem103  31538  fourierdlem104  31539  cbvral2  31672  bnj110  33013  bnj1529  33223
  Copyright terms: Public domain W3C validator