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

Theorem cbvral 2920
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 2571 . 2  |-  F/_ x A
2 nfcv 2571 . 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 2918 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   F/wnf 1553   A.wral 2697
This theorem is referenced by:  cbvralv  2924  cbvralsv  2935  cbviin  4121  disjxun  4202  ralxpf  5010  eqfnfv2f  5822  ralrnmpt  5869  dff13f  5997  ofrfval2  6314  fmpt2x  6408  ovmptss  6419  tfrlem1  6627  cbvixp  7070  mptelixpg  7090  boxcutc  7096  xpf1o  7260  indexfi  7405  ixpiunwdom  7548  dfac8clem  7902  acni2  7916  ac6num  8348  ac6c4  8350  iundom2g  8404  uniimadomf  8409  rlim2  12278  ello1mpt  12303  o1compt  12369  fsum00  12565  iserodd  13197  pcmptdvds  13251  catpropd  13923  invfuc  14159  dprdwd  15557  fiuncmp  17455  elptr2  17594  ptcld  17633  ptclsg  17635  ptcnplem  17641  cnmpt11  17683  cnmpt21  17691  ovoliunlem3  19388  ovoliun  19389  ovoliun2  19390  finiunmbl  19426  volfiniun  19429  iunmbl  19435  voliun  19436  mbfeqalem  19522  mbfsup  19544  mbfinf  19545  mbflim  19548  itg2split  19629  itgeqa  19693  itgfsum  19706  itgabs  19714  itggt0  19721  limciun  19769  dvlipcn  19866  dvfsumlem4  19901  dvfsum2  19906  itgsubst  19921  coeeq2  20149  ulmss  20301  leibpi  20770  rlimcnp  20792  o1cxp  20801  fsumdvdscom  20958  lgseisenlem2  21122  voliune  24573  volfiniune  24574  lgamgulmlem6  24806  itgabsnc  26220  itggt0cn  26223  totbndbnd  26435  climinff  27651  stoweidlem31  27694  cbvral2  27864  bnj110  29083  bnj1529  29293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator