Theorem cbvralw 3304

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1786  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-clel 2811  df-nfc 2886  df-ral 3063

This theorem is referenced by:  cbvralsvw  3315  cbvralsvwOLD  3317  cbviin  5041  disjxun  5147  ralxpf  5847  eqfnfv2f  7037  ralrnmptw  7096  dff13f  7255  ofrfval2  7691  fmpox  8053  ovmptss  8079  cbvixp  8908  mptelixpg  8929  boxcutc  8935  xpf1o  9139  indexfi  9360  ixpiunwdom  9585  dfac8clem  10027  acni2  10041  ac6c4  10476  iundom2g  10535  uniimadomf  10540  rabssnn0fi  13951  rlim2  15440  ello1mpt  15465  o1compt  15531  fsum00  15744  iserodd  16768  pcmptdvds  16827  catpropd  17653  invfuc  17927  gsummptnn0fz  19854  gsummoncoe1  21828  gsumply1eq  21829  fiuncmp  22908  elptr2  23078  ptcld  23117  ptclsg  23119  ptcnplem  23125  cnmpt11  23167  cnmpt21  23175  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  finiunmbl  25061  volfiniun  25064  iunmbl  25070  voliun  25071  mbfeqalem1  25158  mbfsup  25181  mbfinf  25182  mbflim  25185  itg2split  25267  itgeqa  25331  itgfsum  25344  itgabs  25352  itggt0  25361  limciun  25411  dvlipcn  25511  dvfsumlem4  25546  dvfsum2  25551  itgsubst  25566  coeeq2  25756  ulmss  25909  leibpi  26447  rlimcnp  26470  o1cxp  26479  lgamgulmlem6  26538  fsumdvdscom  26689  lgseisenlem2  26879  disjunsn  31856  bnj110  33900  bnj1529  34112  poimirlem23  36559  itgabsnc  36605  itggt0cn  36606  totbndbnd  36705  disjinfi  43939  fmptf  43990  caucvgbf  44248  climinff  44375  idlimc  44390  fnlimabslt  44443  limsupref  44449  limsupbnd1f  44450  climbddf  44451  climinf2  44471  limsupubuz  44477  climinfmpt  44479  limsupmnf  44485  limsupre2  44489  limsupmnfuz  44491  limsupre3  44497  limsupre3uz  44500  limsupreuz  44501  climuz  44508  lmbr3  44511  limsupgt  44542  liminfreuz  44567  liminflt  44569  xlimpnfxnegmnf  44578  xlimmnf  44605  xlimpnf  44606  dfxlim2  44612  cncfshift  44638  stoweidlem31  44795  iundjiun  45224  meaiunincf  45247  pimgtmnf2  45478  smfpimcc  45572  smfsup  45578  smfinflem  45581  smfinf  45582  cbvral2  45859