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  31825  bnj110  33869  bnj1529  34081  poimirlem23  36511  itgabsnc  36557  itggt0cn  36558  totbndbnd  36657  disjinfi  43891  fmptf  43942  caucvgbf  44200  climinff  44327  idlimc  44342  fnlimabslt  44395  limsupref  44401  limsupbnd1f  44402  climbddf  44403  climinf2  44423  limsupubuz  44429  climinfmpt  44431  limsupmnf  44437  limsupre2  44441  limsupmnfuz  44443  limsupre3  44449  limsupre3uz  44452  limsupreuz  44453  climuz  44460  lmbr3  44463  limsupgt  44494  liminfreuz  44519  liminflt  44521  xlimpnfxnegmnf  44530  xlimmnf  44557  xlimpnf  44558  dfxlim2  44564  cncfshift  44590  stoweidlem31  44747  iundjiun  45176  meaiunincf  45199  pimgtmnf2  45430  smfpimcc  45524  smfsup  45530  smfinflem  45533  smfinf  45534  cbvral2  45811