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

Theorem cbvral 2760
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 2419 . 2  |-  F/_ x A
2 nfcv 2419 . 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 2758 1  |-  ( A. x  e.  A  ph  <->  A. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   F/wnf 1531   A.wral 2543
This theorem is referenced by:  cbvralv  2764  cbvralsv  2775  cbviin  3940  disjxun  4021  ralxpf  4830  eqfnfv2f  5626  ralrnmpt  5669  dff13f  5784  ofrfval2  6096  fmpt2x  6190  ovmptss  6200  tfrlem1  6391  cbvixp  6833  mptelixpg  6853  boxcutc  6859  xpf1o  7023  indexfi  7163  ixpiunwdom  7305  dfac8clem  7659  acni2  7673  ac6num  8106  ac6c4  8108  iundom2g  8162  uniimadomf  8167  rlim2  11970  ello1mpt  11995  o1compt  12061  fsum00  12256  iserodd  12888  pcmptdvds  12942  catpropd  13612  invfuc  13848  dprdwd  15246  fiuncmp  17131  elptr2  17269  ptcld  17307  ptclsg  17309  ptcnplem  17315  cnmpt11  17357  cnmpt21  17365  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  finiunmbl  18901  volfiniun  18904  iunmbl  18910  voliun  18911  mbfeqalem  18997  mbfsup  19019  mbfinf  19020  mbflim  19023  itg2split  19104  itgeqa  19168  itgfsum  19181  itgabs  19189  itggt0  19196  limciun  19244  dvlipcn  19341  dvfsumlem4  19376  dvfsum2  19381  itgsubst  19396  coeeq2  19624  ulmss  19774  leibpi  20238  rlimcnp  20260  o1cxp  20269  fsumdvdscom  20425  lgseisenlem2  20589  lmdvg  23376  totbndbnd  26513  climsuse  27734  climinff  27737  stoweidlem7  27756  stoweidlem15  27764  stoweidlem31  27780  wallispilem3  27816  cbvral2  27950  bnj110  28890  bnj1529  29100
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator