Theorem cbvralw 3309

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-11 2195  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2840  df-nfc 2914  df-ral 3082

This theorem is used by:  cbvralsvwOLD  3320  cbviin  5002  disjxun  5109  ralxpf  5834  eqfnfv2f  7033  ralrnmptw  7093  dff13f  7258  ofrfval2  7705  fmpox  8070  ovmptss  8094  cbvixp  8918  mptelixpg  8939  boxcutc  8945  xpf1o  9134  indexfi  9324  ixpiunwdom  9559  dfac8clem  10032  acni2  10046  ac6c4  10480  iundom2g  10539  uniimadomf  10544  rabssnn0fi  14040  rlim2  15571  ello1mpt  15596  o1compt  15662  fsum00  15873  iserodd  16917  pcmptdvds  16976  catpropd  17787  invfuc  18056  gsummptnn0fz  20100  gsummoncoe1  22518  gsumply1eq  22519  fiuncmp  23611  elptr2  23782  ptcld  23821  ptclsg  23823  ptcnplem  23829  cnmpt11  23871  cnmpt21  23879  ovoliunlem3  25714  ovoliun  25715  ovoliun2  25716  finiunmbl  25754  volfiniun  25757  iunmbl  25763  voliun  25764  mbfeqalem1  25851  mbfsup  25874  mbfinf  25875  mbflim  25878  itg2split  25959  itgeqa  26024  itgfsum  26037  itgabs  26045  itggt0  26054  limciun  26104  dvlipcn  26204  dvfsumlem4  26239  dvfsum2  26244  itgsubst  26259  coeeq2  26450  ulmss  26611  leibpi  27158  rlimcnp  27181  o1cxp  27190  lgamgulmlem6  27249  fsumdvdscom  27400  lgseisenlem2  27591  disjunsn  33010  bnj110  35311  bnj1529  35523  weiunpo  37033  weiunso  37034  weiunfr  37035  weiunse  37036  poimirlem23  38351  itgabsnc  38397  itggt0cn  38398  totbndbnd  38498  aks6d1c1p5  42937  aks6d1c1rh  42950  aks6d1c7  43009  unitscyglem3  43022  disjinfi  45968  fmptf  46012  caucvgbf  46261  climinff  46385  idlimc  46400  fnlimabslt  46451  limsupref  46457  limsupbnd1f  46458  climbddf  46459  climinf2  46479  limsupubuz  46485  climinfmpt  46487  limsupmnf  46493  limsupre2  46497  limsupmnfuz  46499  limsupre3  46505  limsupre3uz  46508  limsupreuz  46509  climuz  46516  lmbr3  46519  limsupgt  46550  liminfreuz  46575  liminflt  46577  xlimpnfxnegmnf  46586  xlimmnf  46613  xlimpnf  46614  dfxlim2  46620  cncfshift  46646  stoweidlem31  46803  iundjiun  47232  meaiunincf  47255  pimgtmnf2  47486  smfpimcc  47580  smfsup  47586  smfinflem  47589  smfinf  47590  cbvral2  47898