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

Theorem cbvral 2845
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 2502 . 2  |-  F/_ x A
2 nfcv 2502 . 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 2843 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1549   A.wral 2628
This theorem is referenced by:  cbvralv  2849  cbvralsv  2860  cbviin  4042  disjxun  4123  ralxpf  4933  eqfnfv2f  5733  ralrnmpt  5780  dff13f  5906  ofrfval2  6223  fmpt2x  6317  ovmptss  6328  tfrlem1  6533  cbvixp  6976  mptelixpg  6996  boxcutc  7002  xpf1o  7166  indexfi  7310  ixpiunwdom  7452  dfac8clem  7806  acni2  7820  ac6num  8253  ac6c4  8255  iundom2g  8309  uniimadomf  8314  rlim2  12177  ello1mpt  12202  o1compt  12268  fsum00  12464  iserodd  13096  pcmptdvds  13150  catpropd  13822  invfuc  14058  dprdwd  15456  fiuncmp  17348  elptr2  17486  ptcld  17524  ptclsg  17526  ptcnplem  17532  cnmpt11  17574  cnmpt21  17582  ovoliunlem3  19078  ovoliun  19079  ovoliun2  19080  finiunmbl  19116  volfiniun  19119  iunmbl  19125  voliun  19126  mbfeqalem  19212  mbfsup  19234  mbfinf  19235  mbflim  19238  itg2split  19319  itgeqa  19383  itgfsum  19396  itgabs  19404  itggt0  19411  limciun  19459  dvlipcn  19556  dvfsumlem4  19591  dvfsum2  19596  itgsubst  19611  coeeq2  19839  ulmss  19991  leibpi  20460  rlimcnp  20482  o1cxp  20491  fsumdvdscom  20648  lgseisenlem2  20812  neiptopnei  23644  lmdvg  23693  ustuqtop  23749  voliune  24048  volfiniune  24049  lgamgulmlem6  24266  itgabsnc  25692  itggt0cn  25695  totbndbnd  26019  climsuse  27240  climinff  27243  stoweidlem7  27262  stoweidlem15  27270  stoweidlem31  27286  wallispilem3  27322  cbvral2  27456  bnj110  28654  bnj1529  28864
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633
  Copyright terms: Public domain W3C validator