Theorem cbvralw 3280

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1785  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2812  df-nfc 2886  df-ral 3053

This theorem is referenced by:  cbvralsvwOLD  3291  cbviin  4979  disjxun  5084  ralxpf  5796  eqfnfv2f  6982  ralrnmptw  7041  dff13f  7204  ofrfval2  7646  fmpox  8014  ovmptss  8037  cbvixp  8856  mptelixpg  8877  boxcutc  8883  xpf1o  9071  indexfi  9264  ixpiunwdom  9499  dfac8clem  9948  acni2  9962  ac6c4  10397  iundom2g  10456  uniimadomf  10461  rabssnn0fi  13942  rlim2  15452  ello1mpt  15477  o1compt  15543  fsum00  15755  iserodd  16800  pcmptdvds  16859  catpropd  17669  invfuc  17938  gsummptnn0fz  19955  gsummoncoe1  22286  gsumply1eq  22287  fiuncmp  23382  elptr2  23552  ptcld  23591  ptclsg  23593  ptcnplem  23599  cnmpt11  23641  cnmpt21  23649  ovoliunlem3  25484  ovoliun  25485  ovoliun2  25486  finiunmbl  25524  volfiniun  25527  iunmbl  25533  voliun  25534  mbfeqalem1  25621  mbfsup  25644  mbfinf  25645  mbflim  25648  itg2split  25729  itgeqa  25794  itgfsum  25807  itgabs  25815  itggt0  25824  limciun  25874  dvlipcn  25974  dvfsumlem4  26009  dvfsum2  26014  itgsubst  26029  coeeq2  26220  ulmss  26378  leibpi  26922  rlimcnp  26945  o1cxp  26955  lgamgulmlem6  27014  fsumdvdscom  27165  lgseisenlem2  27356  disjunsn  32682  bnj110  35019  bnj1529  35231  weiunpo  36666  weiunso  36667  weiunfr  36668  weiunse  36669  poimirlem23  37981  itgabsnc  38027  itggt0cn  38028  totbndbnd  38127  aks6d1c1p5  42568  aks6d1c1rh  42581  aks6d1c7  42640  unitscyglem3  42653  disjinfi  45643  fmptf  45689  caucvgbf  45938  climinff  46062  idlimc  46077  fnlimabslt  46128  limsupref  46134  limsupbnd1f  46135  climbddf  46136  climinf2  46156  limsupubuz  46162  climinfmpt  46164  limsupmnf  46170  limsupre2  46174  limsupmnfuz  46176  limsupre3  46182  limsupre3uz  46185  limsupreuz  46186  climuz  46193  lmbr3  46196  limsupgt  46227  liminfreuz  46252  liminflt  46254  xlimpnfxnegmnf  46263  xlimmnf  46290  xlimpnf  46291  dfxlim2  46297  cncfshift  46323  stoweidlem31  46480  iundjiun  46909  meaiunincf  46932  pimgtmnf2  47163  smfpimcc  47257  smfsup  47263  smfinflem  47266  smfinf  47267  cbvral2  47566