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

Theorem cbvral 2941
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 2577 . 2  |-  F/_ x A
2 nfcv 2577 . 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 2939 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 1594   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718
This theorem is referenced by:  cbvralv  2945  cbvralsv  2956  cbviin  4205  disjxun  4287  ralxpf  4982  eqfnfv2f  5798  ralrnmpt  5849  dff13f  5970  ofrfval2  6336  fmpt2x  6639  ovmptss  6653  cbvixp  7276  mptelixpg  7296  boxcutc  7302  xpf1o  7469  indexfi  7615  ixpiunwdom  7802  dfac8clem  8198  acni2  8212  ac6num  8644  ac6c4  8646  iundom2g  8700  uniimadomf  8705  rlim2  12970  ello1mpt  12995  o1compt  13061  fsum00  13257  iserodd  13898  pcmptdvds  13952  catpropd  14644  invfuc  14880  dprdwd  16485  dprdwdOLD  16491  fiuncmp  18907  elptr2  19047  ptcld  19086  ptclsg  19088  ptcnplem  19094  cnmpt11  19136  cnmpt21  19144  ovoliunlem3  20887  ovoliun  20888  ovoliun2  20889  finiunmbl  20925  volfiniun  20928  iunmbl  20934  voliun  20935  mbfeqalem  21020  mbfsup  21042  mbfinf  21043  mbflim  21046  itg2split  21127  itgeqa  21191  itgfsum  21204  itgabs  21212  itggt0  21219  limciun  21269  dvlipcn  21366  dvfsumlem4  21401  dvfsum2  21406  itgsubst  21421  coeeq2  21653  ulmss  21805  leibpi  22280  rlimcnp  22302  o1cxp  22311  fsumdvdscom  22468  lgseisenlem2  22632  disjunsn  25855  nn0min  26007  voliune  26565  volfiniune  26566  lgamgulmlem6  26934  itgabsnc  28370  itggt0cn  28373  totbndbnd  28597  climinff  29693  stoweidlem31  29735  cbvral2  29905  bnj110  31668  bnj1529  31878
  Copyright terms: Public domain W3C validator