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

Theorem cbvral 2762
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 2421 . 2  |-  F/_ x A
2 nfcv 2421 . 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 2760 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178   F/wnf 1532   A.wral 2545
This theorem is referenced by:  cbvralv  2766  cbvralsv  2777  cbviin  3942  disjxun  4023  ralxpf  4830  eqfnfv2f  5588  ralrnmpt  5631  dff13f  5746  ofrfval2  6058  fmpt2x  6152  ovmptss  6162  tfrlem1  6387  cbvixp  6829  mptelixpg  6849  boxcutc  6855  xpf1o  7019  indexfi  7159  ixpiunwdom  7301  dfac8clem  7655  acni2  7669  ac6num  8102  ac6c4  8104  iundom2g  8158  uniimadomf  8163  rlim2  11965  ello1mpt  11990  o1compt  12056  fsum00  12251  iserodd  12883  pcmptdvds  12937  catpropd  13607  invfuc  13843  dprdwd  15241  fiuncmp  17126  elptr2  17264  ptcld  17302  ptclsg  17304  ptcnplem  17310  cnmpt11  17352  cnmpt21  17360  ovoliunlem3  18858  ovoliun  18859  ovoliun2  18860  finiunmbl  18896  volfiniun  18899  iunmbl  18905  voliun  18906  mbfeqalem  18992  mbfsup  19014  mbfinf  19015  mbflim  19018  itg2split  19099  itgeqa  19163  itgfsum  19176  itgabs  19184  itggt0  19191  limciun  19239  dvlipcn  19336  dvfsumlem4  19371  dvfsum2  19376  itgsubst  19391  coeeq2  19619  ulmss  19769  leibpi  20233  rlimcnp  20255  o1cxp  20264  fsumdvdscom  20420  lgseisenlem2  20584  totbndbnd  25913  climsuse  27134  climinff  27137  stoweidlem7  27156  stoweidlem15  27164  stoweidlem31  27180  wallispilem3  27216  cbvral2  27330  bnj110  28158  bnj1529  28368
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ral 2550
  Copyright terms: Public domain W3C validator