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 2403. (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 2924	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2924	. 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 208  Ⅎwnf 1803  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-11 2191  ax-12 2212

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-nf 1804  df-clel 2837  df-nfc 2911  df-ral 3077

This theorem is referenced by:  cbvralsvwOLD  3315  cbviin  4993  disjxun  5098  ralxpf  5818  eqfnfv2f  7015  ralrnmptw  7075  dff13f  7239  ofrfval2  7681  fmpox  8048  ovmptss  8072  cbvixp  8896  mptelixpg  8917  boxcutc  8923  xpf1o  9111  indexfi  9303  ixpiunwdom  9538  dfac8clem  9988  acni2  10002  ac6c4  10438  iundom2g  10497  uniimadomf  10502  rabssnn0fi  13999  rlim2  15523  ello1mpt  15548  o1compt  15614  fsum00  15826  iserodd  16871  pcmptdvds  16930  catpropd  17741  invfuc  18010  gsummptnn0fz  20026  gsummoncoe1  22371  gsumply1eq  22372  fiuncmp  23464  elptr2  23634  ptcld  23673  ptclsg  23675  ptcnplem  23681  cnmpt11  23723  cnmpt21  23731  ovoliunlem3  25566  ovoliun  25567  ovoliun2  25568  finiunmbl  25606  volfiniun  25609  iunmbl  25615  voliun  25616  mbfeqalem1  25703  mbfsup  25726  mbfinf  25727  mbflim  25730  itg2split  25811  itgeqa  25876  itgfsum  25889  itgabs  25897  itggt0  25906  limciun  25956  dvlipcn  26056  dvfsumlem4  26091  dvfsum2  26096  itgsubst  26111  coeeq2  26302  ulmss  26460  leibpi  27007  rlimcnp  27030  o1cxp  27039  lgamgulmlem6  27098  fsumdvdscom  27249  lgseisenlem2  27440  disjunsn  32794  bnj110  35153  bnj1529  35365  weiunpo  36825  weiunso  36826  weiunfr  36827  weiunse  36828  poimirlem23  38142  itgabsnc  38188  itggt0cn  38189  totbndbnd  38288  aks6d1c1p5  42729  aks6d1c1rh  42742  aks6d1c7  42801  unitscyglem3  42814  disjinfi  45770  fmptf  45814  caucvgbf  46063  climinff  46187  idlimc  46202  fnlimabslt  46253  limsupref  46259  limsupbnd1f  46260  climbddf  46261  climinf2  46281  limsupubuz  46287  climinfmpt  46289  limsupmnf  46295  limsupre2  46299  limsupmnfuz  46301  limsupre3  46307  limsupre3uz  46310  limsupreuz  46311  climuz  46318  lmbr3  46321  limsupgt  46352  liminfreuz  46377  liminflt  46379  xlimpnfxnegmnf  46388  xlimmnf  46415  xlimpnf  46416  dfxlim2  46422  cncfshift  46448  stoweidlem31  46605  iundjiun  47034  meaiunincf  47057  pimgtmnf2  47288  smfpimcc  47382  smfsup  47388  smfinflem  47391  smfinf  47392  cbvral2  47697