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

Theorem cbvral 3080
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 2619 . 2  |-  F/_ x A
2 nfcv 2619 . 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 3078 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   F/wnf 1617   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1614  df-nf 1618  df-sb 1741  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812
This theorem is referenced by:  cbvralv  3084  cbvralsv  3095  cbviin  4370  disjxun  4454  ralxpf  5159  eqfnfv2f  5986  ralrnmpt  6041  dff13f  6168  ofrfval2  6556  fmpt2x  6865  ovmptss  6880  cbvixp  7505  mptelixpg  7525  boxcutc  7531  xpf1o  7698  indexfi  7846  ixpiunwdom  8035  dfac8clem  8430  acni2  8444  ac6num  8876  ac6c4  8878  iundom2g  8932  uniimadomf  8937  rabssnn0fi  12097  rlim2  13330  ello1mpt  13355  o1compt  13421  fsum00  13623  iserodd  14370  pcmptdvds  14424  catpropd  15124  invfuc  15389  gsummptnn0fz  17140  dprdwdOLD2  17171  dprdwdOLD  17177  gsummoncoe1  18472  gsumply1eq  18473  fiuncmp  20030  elptr2  20200  ptcld  20239  ptclsg  20241  ptcnplem  20247  cnmpt11  20289  cnmpt21  20297  ovoliunlem3  22040  ovoliun  22041  ovoliun2  22042  finiunmbl  22079  volfiniun  22082  iunmbl  22088  voliun  22089  mbfeqalem  22174  mbfsup  22196  mbfinf  22197  mbflim  22200  itg2split  22281  itgeqa  22345  itgfsum  22358  itgabs  22366  itggt0  22373  limciun  22423  dvlipcn  22520  dvfsumlem4  22555  dvfsum2  22560  itgsubst  22575  coeeq2  22764  ulmss  22917  leibpi  23398  rlimcnp  23420  o1cxp  23429  fsumdvdscom  23586  lgseisenlem2  23750  disjunsn  27590  lgamgulmlem6  28751  itgabsnc  30246  itggt0cn  30249  totbndbnd  30447  climinff  31778  idlimc  31793  cncfshift  31837  stoweidlem31  31974  cbvral2  32338  bnj110  34017  bnj1529  34227
  Copyright terms: Public domain W3C validator