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

Theorem cbvral 2930
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 2574 . 2  |-  F/_ x A
2 nfcv 2574 . 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 2928 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   F/wnf 1554   A.wral 2707
This theorem is referenced by:  cbvralv  2934  cbvralsv  2945  cbviin  4131  disjxun  4213  ralxpf  5022  eqfnfv2f  5834  ralrnmpt  5881  dff13f  6009  ofrfval2  6326  fmpt2x  6420  ovmptss  6431  tfrlem1  6639  cbvixp  7082  mptelixpg  7102  boxcutc  7108  xpf1o  7272  indexfi  7417  ixpiunwdom  7562  dfac8clem  7918  acni2  7932  ac6num  8364  ac6c4  8366  iundom2g  8420  uniimadomf  8425  rlim2  12295  ello1mpt  12320  o1compt  12386  fsum00  12582  iserodd  13214  pcmptdvds  13268  catpropd  13940  invfuc  14176  dprdwd  15574  fiuncmp  17472  elptr2  17611  ptcld  17650  ptclsg  17652  ptcnplem  17658  cnmpt11  17700  cnmpt21  17708  ovoliunlem3  19405  ovoliun  19406  ovoliun2  19407  finiunmbl  19443  volfiniun  19446  iunmbl  19452  voliun  19453  mbfeqalem  19537  mbfsup  19559  mbfinf  19560  mbflim  19563  itg2split  19644  itgeqa  19708  itgfsum  19721  itgabs  19729  itggt0  19736  limciun  19786  dvlipcn  19883  dvfsumlem4  19918  dvfsum2  19923  itgsubst  19938  coeeq2  20166  ulmss  20318  leibpi  20787  rlimcnp  20809  o1cxp  20818  fsumdvdscom  20975  lgseisenlem2  21139  voliune  24590  volfiniune  24591  lgamgulmlem6  24823  itgabsnc  26288  itggt0cn  26291  totbndbnd  26512  climinff  27727  stoweidlem31  27770  cbvral2  27940  bnj110  29303  bnj1529  29513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712
  Copyright terms: Public domain W3C validator