Theorem cbvralw 3281

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3279 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2380. (Revised by GG, 10-Jan-2024.)

Hypotheses

Ref	Expression
cbvralw.1	⊢ Ⅎ𝑦𝜑
cbvralw.2	⊢ Ⅎ𝑥𝜓
cbvralw.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralw	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable group:   𝑥,𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem cbvralw

Step	Hyp	Ref	Expression
1		nfcv 2901	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2901	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3279	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 207  Ⅎwnf 1790  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-11 2168  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-clel 2814  df-nfc 2888  df-ral 3054

This theorem is referenced by:  cbvralsvwOLD  3292  cbviin  4965  disjxun  5070  ralxpf  5788  eqfnfv2f  6975  ralrnmptw  7035  dff13f  7199  ofrfval2  7641  fmpox  8009  ovmptss  8032  cbvixp  8852  mptelixpg  8873  boxcutc  8879  xpf1o  9067  indexfi  9260  ixpiunwdom  9495  dfac8clem  9945  acni2  9959  ac6c4  10394  iundom2g  10453  uniimadomf  10458  rabssnn0fi  13939  rlim2  15449  ello1mpt  15474  o1compt  15540  fsum00  15752  iserodd  16797  pcmptdvds  16856  catpropd  17666  invfuc  17935  gsummptnn0fz  19952  gsummoncoe1  22294  gsumply1eq  22295  fiuncmp  23387  elptr2  23557  ptcld  23596  ptclsg  23598  ptcnplem  23604  cnmpt11  23646  cnmpt21  23654  ovoliunlem3  25489  ovoliun  25490  ovoliun2  25491  finiunmbl  25529  volfiniun  25532  iunmbl  25538  voliun  25539  mbfeqalem1  25626  mbfsup  25649  mbfinf  25650  mbflim  25653  itg2split  25734  itgeqa  25799  itgfsum  25812  itgabs  25820  itggt0  25829  limciun  25879  dvlipcn  25979  dvfsumlem4  26014  dvfsum2  26019  itgsubst  26034  coeeq2  26225  ulmss  26380  leibpi  26924  rlimcnp  26947  o1cxp  26956  lgamgulmlem6  27015  fsumdvdscom  27166  lgseisenlem2  27357  disjunsn  32683  bnj110  35040  bnj1529  35252  weiunpo  36693  weiunso  36694  weiunfr  36695  weiunse  36696  poimirlem23  38010  itgabsnc  38056  itggt0cn  38057  totbndbnd  38156  aks6d1c1p5  42597  aks6d1c1rh  42610  aks6d1c7  42669  unitscyglem3  42682  disjinfi  45639  fmptf  45683  caucvgbf  45932  climinff  46056  idlimc  46071  fnlimabslt  46122  limsupref  46128  limsupbnd1f  46129  climbddf  46130  climinf2  46150  limsupubuz  46156  climinfmpt  46158  limsupmnf  46164  limsupre2  46168  limsupmnfuz  46170  limsupre3  46176  limsupre3uz  46179  limsupreuz  46180  climuz  46187  lmbr3  46190  limsupgt  46221  liminfreuz  46246  liminflt  46248  xlimpnfxnegmnf  46257  xlimmnf  46284  xlimpnf  46285  dfxlim2  46291  cncfshift  46317  stoweidlem31  46474  iundjiun  46903  meaiunincf  46926  pimgtmnf2  47157  smfpimcc  47251  smfsup  47257  smfinflem  47260  smfinf  47261  cbvral2  47566