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

Theorem cbvral 3306
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.)
Hypotheses
Ref Expression
cbvral.1 𝑦𝜑
cbvral.2 𝑥𝜓
cbvral.3 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvral (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvral
StepHypRef Expression
1 nfcv 2902 . 2 𝑥𝐴
2 nfcv 2902 . 2 𝑦𝐴
3 cbvral.1 . 2 𝑦𝜑
4 cbvral.2 . 2 𝑥𝜓
5 cbvral.3 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvralf 3304 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wnf 1857  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clel 2756  df-nfc 2891  df-ral 3055
This theorem is referenced by:  cbvralv  3310  cbvralsv  3321  cbviin  4710  disjxun  4802  ralxpf  5424  eqfnfv2f  6478  ralrnmpt  6531  dff13f  6676  ofrfval2  7080  fmpt2x  7404  ovmptss  7426  cbvixp  8091  mptelixpg  8111  boxcutc  8117  xpf1o  8287  indexfi  8439  ixpiunwdom  8661  dfac8clem  9045  acni2  9059  ac6num  9493  ac6c4  9495  iundom2g  9554  uniimadomf  9559  rabssnn0fi  12979  rlim2  14426  ello1mpt  14451  o1compt  14517  fsum00  14729  iserodd  15742  pcmptdvds  15800  catpropd  16570  invfuc  16835  gsummptnn0fz  18582  gsummoncoe1  19876  gsumply1eq  19877  fiuncmp  21409  elptr2  21579  ptcld  21618  ptclsg  21620  ptcnplem  21626  cnmpt11  21668  cnmpt21  21676  ovoliunlem3  23472  ovoliun  23473  ovoliun2  23474  finiunmbl  23512  volfiniun  23515  iunmbl  23521  voliun  23522  mbfeqalem  23608  mbfsup  23630  mbfinf  23631  mbflim  23634  itg2split  23715  itgeqa  23779  itgfsum  23792  itgabs  23800  itggt0  23807  limciun  23857  dvlipcn  23956  dvfsumlem4  23991  dvfsum2  23996  itgsubst  24011  coeeq2  24197  ulmss  24350  leibpi  24868  rlimcnp  24891  o1cxp  24900  lgamgulmlem6  24959  fsumdvdscom  25110  lgseisenlem2  25300  disjunsn  29714  bnj110  31235  bnj1529  31445  poimirlem23  33745  itgabsnc  33792  itggt0cn  33795  totbndbnd  33901  disjinfi  39879  fmptf  39947  climinff  40346  idlimc  40361  fnlimabslt  40414  limsupref  40420  limsupbnd1f  40421  climbddf  40422  climinf2  40442  limsupubuz  40448  climinfmpt  40450  limsupmnf  40456  limsupre2  40460  limsupmnfuz  40462  limsupre3  40468  limsupre3uz  40471  limsupreuz  40472  climuz  40479  lmbr3  40482  liminflelimsup  40511  limsupgt  40513  liminfreuz  40538  liminflt  40540  xlimmnf  40570  xlimpnf  40571  dfxlim2  40577  cncfshift  40590  stoweidlem31  40751  iundjiun  41180  meaiunincf  41203  pimgtmnf2  41430  smfpimcc  41520  smfsup  41526  smfinflem  41529  smfinf  41530  cbvral2  41678
  Copyright terms: Public domain W3C validator