Theorem cbvralw 3278

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-11 2162  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2811  df-nfc 2885  df-ral 3052

This theorem is referenced by:  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbviin  4991  disjxun  5096  ralxpf  5795  eqfnfv2f  6980  ralrnmptw  7039  dff13f  7201  ofrfval2  7643  fmpox  8011  ovmptss  8035  cbvixp  8852  mptelixpg  8873  boxcutc  8879  xpf1o  9067  indexfi  9260  ixpiunwdom  9495  dfac8clem  9942  acni2  9956  ac6c4  10391  iundom2g  10450  uniimadomf  10455  rabssnn0fi  13909  rlim2  15419  ello1mpt  15444  o1compt  15510  fsum00  15721  iserodd  16763  pcmptdvds  16822  catpropd  17632  invfuc  17901  gsummptnn0fz  19915  gsummoncoe1  22252  gsumply1eq  22253  fiuncmp  23348  elptr2  23518  ptcld  23557  ptclsg  23559  ptcnplem  23565  cnmpt11  23607  cnmpt21  23615  ovoliunlem3  25461  ovoliun  25462  ovoliun2  25463  finiunmbl  25501  volfiniun  25504  iunmbl  25510  voliun  25511  mbfeqalem1  25598  mbfsup  25621  mbfinf  25622  mbflim  25625  itg2split  25706  itgeqa  25771  itgfsum  25784  itgabs  25792  itggt0  25801  limciun  25851  dvlipcn  25955  dvfsumlem4  25992  dvfsum2  25997  itgsubst  26012  coeeq2  26203  ulmss  26362  leibpi  26908  rlimcnp  26931  o1cxp  26941  lgamgulmlem6  27000  fsumdvdscom  27151  lgseisenlem2  27343  disjunsn  32669  bnj110  35014  bnj1529  35226  weiunpo  36659  weiunso  36660  weiunfr  36661  weiunse  36662  poimirlem23  37844  itgabsnc  37890  itggt0cn  37891  totbndbnd  37990  aks6d1c1p5  42366  aks6d1c1rh  42379  aks6d1c7  42438  unitscyglem3  42451  disjinfi  45436  fmptf  45483  caucvgbf  45733  climinff  45857  idlimc  45872  fnlimabslt  45923  limsupref  45929  limsupbnd1f  45930  climbddf  45931  climinf2  45951  limsupubuz  45957  climinfmpt  45959  limsupmnf  45965  limsupre2  45969  limsupmnfuz  45971  limsupre3  45977  limsupre3uz  45980  limsupreuz  45981  climuz  45988  lmbr3  45991  limsupgt  46022  liminfreuz  46047  liminflt  46049  xlimpnfxnegmnf  46058  xlimmnf  46085  xlimpnf  46086  dfxlim2  46092  cncfshift  46118  stoweidlem31  46275  iundjiun  46704  meaiunincf  46727  pimgtmnf2  46958  smfpimcc  47052  smfsup  47058  smfinflem  47061  smfinf  47062  cbvral2  47349