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

Theorem cbvral 2943
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 2579 . 2  |-  F/_ x A
2 nfcv 2579 . 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 2941 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 1589   A.wral 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720
This theorem is referenced by:  cbvralv  2947  cbvralsv  2958  cbviin  4208  disjxun  4290  ralxpf  4986  eqfnfv2f  5801  ralrnmpt  5852  dff13f  5973  ofrfval2  6337  fmpt2x  6640  ovmptss  6654  cbvixp  7280  mptelixpg  7300  boxcutc  7306  xpf1o  7473  indexfi  7619  ixpiunwdom  7806  dfac8clem  8202  acni2  8216  ac6num  8648  ac6c4  8650  iundom2g  8704  uniimadomf  8709  rlim2  12974  ello1mpt  12999  o1compt  13065  fsum00  13261  iserodd  13902  pcmptdvds  13956  catpropd  14648  invfuc  14884  dprdwd  16495  dprdwdOLD  16501  fiuncmp  19007  elptr2  19147  ptcld  19186  ptclsg  19188  ptcnplem  19194  cnmpt11  19236  cnmpt21  19244  ovoliunlem3  20987  ovoliun  20988  ovoliun2  20989  finiunmbl  21025  volfiniun  21028  iunmbl  21034  voliun  21035  mbfeqalem  21120  mbfsup  21142  mbfinf  21143  mbflim  21146  itg2split  21227  itgeqa  21291  itgfsum  21304  itgabs  21312  itggt0  21319  limciun  21369  dvlipcn  21466  dvfsumlem4  21501  dvfsum2  21506  itgsubst  21521  coeeq2  21710  ulmss  21862  leibpi  22337  rlimcnp  22359  o1cxp  22368  fsumdvdscom  22525  lgseisenlem2  22689  disjunsn  25936  nn0min  26090  voliune  26645  volfiniune  26646  lgamgulmlem6  27020  itgabsnc  28461  itggt0cn  28464  totbndbnd  28688  climinff  29784  stoweidlem31  29826  cbvral2  29996  rabssnn0fi  30747  gsummptnn0fz  30806  gsummoncoe1  30843  bnj110  31851  bnj1529  32061
  Copyright terms: Public domain W3C validator