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

Theorem cbvral 2888
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 2540 . 2  |-  F/_ x A
2 nfcv 2540 . 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 2886 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 1550   A.wral 2666
This theorem is referenced by:  cbvralv  2892  cbvralsv  2903  cbviin  4089  disjxun  4170  ralxpf  4978  eqfnfv2f  5790  ralrnmpt  5837  dff13f  5965  ofrfval2  6282  fmpt2x  6376  ovmptss  6387  tfrlem1  6595  cbvixp  7038  mptelixpg  7058  boxcutc  7064  xpf1o  7228  indexfi  7372  ixpiunwdom  7515  dfac8clem  7869  acni2  7883  ac6num  8315  ac6c4  8317  iundom2g  8371  uniimadomf  8376  rlim2  12245  ello1mpt  12270  o1compt  12336  fsum00  12532  iserodd  13164  pcmptdvds  13218  catpropd  13890  invfuc  14126  dprdwd  15524  fiuncmp  17421  elptr2  17559  ptcld  17598  ptclsg  17600  ptcnplem  17606  cnmpt11  17648  cnmpt21  17656  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  finiunmbl  19391  volfiniun  19394  iunmbl  19400  voliun  19401  mbfeqalem  19487  mbfsup  19509  mbfinf  19510  mbflim  19513  itg2split  19594  itgeqa  19658  itgfsum  19671  itgabs  19679  itggt0  19686  limciun  19734  dvlipcn  19831  dvfsumlem4  19866  dvfsum2  19871  itgsubst  19886  coeeq2  20114  ulmss  20266  leibpi  20735  rlimcnp  20757  o1cxp  20766  fsumdvdscom  20923  lgseisenlem2  21087  voliune  24538  volfiniune  24539  lgamgulmlem6  24771  itgabsnc  26173  itggt0cn  26176  totbndbnd  26388  climinff  27604  stoweidlem31  27647  cbvral2  27817  bnj110  28935  bnj1529  29145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671
  Copyright terms: Public domain W3C validator