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

Theorem cbvral 3051
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 2584 . 2  |-  F/_ x A
2 nfcv 2584 . 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 3049 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   F/wnf 1663   A.wral 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780
This theorem is referenced by:  cbvralv  3055  cbvralsv  3066  cbviin  4334  disjxun  4418  ralxpf  4996  eqfnfv2f  5991  ralrnmpt  6042  dff13f  6171  ofrfval2  6559  fmpt2x  6869  ovmptss  6884  cbvixp  7543  mptelixpg  7563  boxcutc  7569  xpf1o  7736  indexfi  7884  ixpiunwdom  8108  dfac8clem  8463  acni2  8477  ac6num  8909  ac6c4  8911  iundom2g  8965  uniimadomf  8970  rabssnn0fi  12197  rlim2  13547  ello1mpt  13572  o1compt  13638  fsum00  13845  iserodd  14772  pcmptdvds  14826  catpropd  15601  invfuc  15866  gsummptnn0fz  17602  dprdwdOLD  17631  gsummoncoe1  18885  gsumply1eq  18886  fiuncmp  20405  elptr2  20575  ptcld  20614  ptclsg  20616  ptcnplem  20622  cnmpt11  20664  cnmpt21  20672  ovoliunlem3  22443  ovoliun  22444  ovoliun2  22445  finiunmbl  22483  volfiniun  22486  iunmbl  22492  voliun  22493  mbfeqalem  22584  mbfsup  22606  mbfinf  22607  mbfinfOLD  22608  mbflim  22612  itg2split  22693  itgeqa  22757  itgfsum  22770  itgabs  22778  itggt0  22785  limciun  22835  dvlipcn  22932  dvfsumlem4  22967  dvfsum2  22972  itgsubst  22987  coeeq2  23182  ulmss  23338  leibpi  23854  rlimcnp  23877  o1cxp  23886  lgamgulmlem6  23945  fsumdvdscom  24100  lgseisenlem2  24264  disjunsn  28193  bnj110  29664  bnj1529  29874  poimirlem23  31876  itgabsnc  31924  itggt0cn  31927  totbndbnd  32034  disjinfi  37317  climinff  37509  climinffOLD  37510  idlimc  37525  cncfshift  37570  stoweidlem31  37711  iundjiun  38076  cbvral2  38305
  Copyright terms: Public domain W3C validator