Theorem cbvralw 3295

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3293 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2363. (Revised by Gino Giotto, 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 2895	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2895	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3293	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1777  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-11 2146  ax-12 2163

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-nf 1778  df-clel 2802  df-nfc 2877  df-ral 3054

This theorem is referenced by:  cbvralsvw  3306  cbvralsvwOLD  3308  cbviin  5030  disjxun  5136  ralxpf  5836  eqfnfv2f  7026  ralrnmptw  7085  dff13f  7247  ofrfval2  7684  fmpox  8046  ovmptss  8073  cbvixp  8903  mptelixpg  8924  boxcutc  8930  xpf1o  9134  indexfi  9355  ixpiunwdom  9580  dfac8clem  10022  acni2  10036  ac6c4  10471  iundom2g  10530  uniimadomf  10535  rabssnn0fi  13947  rlim2  15436  ello1mpt  15461  o1compt  15527  fsum00  15740  iserodd  16766  pcmptdvds  16825  catpropd  17651  invfuc  17928  gsummptnn0fz  19895  gsummoncoe1  22148  gsumply1eq  22149  fiuncmp  23229  elptr2  23399  ptcld  23438  ptclsg  23440  ptcnplem  23446  cnmpt11  23488  cnmpt21  23496  ovoliunlem3  25354  ovoliun  25355  ovoliun2  25356  finiunmbl  25394  volfiniun  25397  iunmbl  25403  voliun  25404  mbfeqalem1  25491  mbfsup  25514  mbfinf  25515  mbflim  25518  itg2split  25600  itgeqa  25664  itgfsum  25677  itgabs  25685  itggt0  25694  limciun  25744  dvlipcn  25848  dvfsumlem4  25885  dvfsum2  25890  itgsubst  25905  coeeq2  26095  ulmss  26249  leibpi  26789  rlimcnp  26812  o1cxp  26822  lgamgulmlem6  26881  fsumdvdscom  27032  lgseisenlem2  27224  disjunsn  32260  bnj110  34324  bnj1529  34536  poimirlem23  36967  itgabsnc  37013  itggt0cn  37014  totbndbnd  37113  disjinfi  44342  fmptf  44393  caucvgbf  44651  climinff  44778  idlimc  44793  fnlimabslt  44846  limsupref  44852  limsupbnd1f  44853  climbddf  44854  climinf2  44874  limsupubuz  44880  climinfmpt  44882  limsupmnf  44888  limsupre2  44892  limsupmnfuz  44894  limsupre3  44900  limsupre3uz  44903  limsupreuz  44904  climuz  44911  lmbr3  44914  limsupgt  44945  liminfreuz  44970  liminflt  44972  xlimpnfxnegmnf  44981  xlimmnf  45008  xlimpnf  45009  dfxlim2  45015  cncfshift  45041  stoweidlem31  45198  iundjiun  45627  meaiunincf  45650  pimgtmnf2  45881  smfpimcc  45975  smfsup  45981  smfinflem  45984  smfinf  45985  cbvral2  46262