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 2401. (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 2922	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2922	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3302	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 2147  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2835  df-nfc 2909  df-ral 3077

This theorem is used by:  cbviin  4994  disjxun  5101  ralxpf  5826  eqfnfv2f  7026  ralrnmptw  7087  dff13f  7252  ofrfval2  7699  fmpox  8064  ovmptss  8090  cbvixp  8921  mptelixpg  8942  boxcutc  8948  xpf1o  9137  indexfi  9327  ixpiunwdom  9562  dfac8clem  10035  acni2  10049  ac6c4  10483  iundom2g  10548  uniimadomf  10553  rabssnn0fi  14050  rlim2  15583  ello1mpt  15608  o1compt  15674  fsum00  15885  iserodd  16927  pcmptdvds  16986  catpropd  17797  invfuc  18066  gsummptnn0fz  20113  gsummoncoe1  22533  gsumply1eq  22534  fiuncmp  23629  elptr2  23800  ptcld  23839  ptclsg  23841  ptcnplem  23847  cnmpt11  23889  cnmpt21  23897  ovoliunlem3  25732  ovoliun  25733  ovoliun2  25734  finiunmbl  25772  volfiniun  25775  iunmbl  25781  voliun  25782  mbfeqalem1  25869  mbfsup  25892  mbfinf  25893  mbflim  25896  itg2split  25977  itgeqa  26041  itgfsum  26054  itgabs  26062  itggt0  26071  limciun  26121  dvlipcn  26221  dvfsumlem4  26256  dvfsum2  26261  itgsubst  26276  coeeq2  26468  ulmss  26633  leibpi  27179  rlimcnp  27202  o1cxp  27211  lgamgulmlem6  27270  fsumdvdscom  27421  lgseisenlem2  27612  disjunsn  33067  bnj110  35367  bnj1529  35579  weiunpo  37084  weiunso  37085  weiunfr  37086  weiunse  37087  poimirlem23  38392  itgabsnc  38438  itggt0cn  38439  totbndbnd  38539  aks6d1c1p5  42978  aks6d1c1rh  42991  aks6d1c7  43050  unitscyglem3  43063  disjinfi  46024  fmptf  46068  caucvgbf  46317  climinff  46441  idlimc  46456  fnlimabslt  46507  limsupref  46513  limsupbnd1f  46514  climbddf  46515  climinf2  46535  limsupubuz  46541  climinfmpt  46543  limsupmnf  46549  limsupre2  46553  limsupmnfuz  46555  limsupre3  46561  limsupre3uz  46564  limsupreuz  46565  climuz  46572  lmbr3  46575  limsupgt  46606  liminfreuz  46631  liminflt  46633  xlimpnfxnegmnf  46642  xlimmnf  46669  xlimpnf  46670  dfxlim2  46676  cncfshift  46702  stoweidlem31  46859  iundjiun  47288  meaiunincf  47311  pimgtmnf2  47542  smfpimcc  47636  smfsup  47642  smfinflem  47645  smfinf  47646  cbvral2  47991