Theorem cbvralw 3303

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1785  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-clel 2810  df-nfc 2885  df-ral 3062

This theorem is referenced by:  cbvralsvw  3314  cbvralsvwOLD  3316  cbviin  5039  disjxun  5145  ralxpf  5844  eqfnfv2f  7033  ralrnmptw  7092  dff13f  7251  ofrfval2  7687  fmpox  8049  ovmptss  8075  cbvixp  8904  mptelixpg  8925  boxcutc  8931  xpf1o  9135  indexfi  9356  ixpiunwdom  9581  dfac8clem  10023  acni2  10037  ac6c4  10472  iundom2g  10531  uniimadomf  10536  rabssnn0fi  13947  rlim2  15436  ello1mpt  15461  o1compt  15527  fsum00  15740  iserodd  16764  pcmptdvds  16823  catpropd  17649  invfuc  17923  gsummptnn0fz  19848  gsummoncoe1  21819  gsumply1eq  21820  fiuncmp  22899  elptr2  23069  ptcld  23108  ptclsg  23110  ptcnplem  23116  cnmpt11  23158  cnmpt21  23166  ovoliunlem3  25012  ovoliun  25013  ovoliun2  25014  finiunmbl  25052  volfiniun  25055  iunmbl  25061  voliun  25062  mbfeqalem1  25149  mbfsup  25172  mbfinf  25173  mbflim  25176  itg2split  25258  itgeqa  25322  itgfsum  25335  itgabs  25343  itggt0  25352  limciun  25402  dvlipcn  25502  dvfsumlem4  25537  dvfsum2  25542  itgsubst  25557  coeeq2  25747  ulmss  25900  leibpi  26436  rlimcnp  26459  o1cxp  26468  lgamgulmlem6  26527  fsumdvdscom  26678  lgseisenlem2  26868  disjunsn  31812  bnj110  33857  bnj1529  34069  poimirlem23  36499  itgabsnc  36545  itggt0cn  36546  totbndbnd  36645  disjinfi  43876  fmptf  43927  caucvgbf  44186  climinff  44313  idlimc  44328  fnlimabslt  44381  limsupref  44387  limsupbnd1f  44388  climbddf  44389  climinf2  44409  limsupubuz  44415  climinfmpt  44417  limsupmnf  44423  limsupre2  44427  limsupmnfuz  44429  limsupre3  44435  limsupre3uz  44438  limsupreuz  44439  climuz  44446  lmbr3  44449  limsupgt  44480  liminfreuz  44505  liminflt  44507  xlimpnfxnegmnf  44516  xlimmnf  44543  xlimpnf  44544  dfxlim2  44550  cncfshift  44576  stoweidlem31  44733  iundjiun  45162  meaiunincf  45185  pimgtmnf2  45416  smfpimcc  45510  smfsup  45516  smfinflem  45519  smfinf  45520  cbvral2  45797