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

Theorem cbvral 3027
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 2603 . 2  |-  F/_ x A
2 nfcv 2603 . 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 3025 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   F/wnf 1678   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-ex 1675  df-nf 1679  df-sb 1809  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754
This theorem is referenced by:  cbvralv  3031  cbvralsv  3042  cbviin  4330  disjxun  4414  ralxpf  5000  eqfnfv2f  6003  ralrnmpt  6054  dff13f  6185  ofrfval2  6576  fmpt2x  6886  ovmptss  6904  cbvixp  7565  mptelixpg  7585  boxcutc  7591  xpf1o  7760  indexfi  7908  ixpiunwdom  8132  dfac8clem  8489  acni2  8503  ac6num  8935  ac6c4  8937  iundom2g  8991  uniimadomf  8996  rabssnn0fi  12230  rlim2  13609  ello1mpt  13634  o1compt  13700  fsum00  13907  iserodd  14834  pcmptdvds  14888  catpropd  15663  invfuc  15928  gsummptnn0fz  17664  dprdwdOLD  17693  gsummoncoe1  18947  gsumply1eq  18948  fiuncmp  20468  elptr2  20638  ptcld  20677  ptclsg  20679  ptcnplem  20685  cnmpt11  20727  cnmpt21  20735  ovoliunlem3  22506  ovoliun  22507  ovoliun2  22508  finiunmbl  22546  volfiniun  22549  iunmbl  22555  voliun  22556  mbfeqalem  22647  mbfsup  22669  mbfinf  22670  mbfinfOLD  22671  mbflim  22675  itg2split  22756  itgeqa  22820  itgfsum  22833  itgabs  22841  itggt0  22848  limciun  22898  dvlipcn  22995  dvfsumlem4  23030  dvfsum2  23035  itgsubst  23050  coeeq2  23245  ulmss  23401  leibpi  23917  rlimcnp  23940  o1cxp  23949  lgamgulmlem6  24008  fsumdvdscom  24163  lgseisenlem2  24327  disjunsn  28253  bnj110  29718  bnj1529  29928  poimirlem23  32008  itgabsnc  32056  itggt0cn  32059  totbndbnd  32166  disjinfi  37506  climinff  37728  climinffOLD  37729  idlimc  37744  cncfshift  37789  stoweidlem31  37930  iundjiun  38336  cbvral2  38631
  Copyright terms: Public domain W3C validator