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  cbvralsvwOLDOLD  3292  cbviin  4993  disjxun  5098  ralxpf  5803  eqfnfv2f  6989  ralrnmptw  7048  dff13f  7211  ofrfval2  7653  fmpox  8021  ovmptss  8045  cbvixp  8864  mptelixpg  8885  boxcutc  8891  xpf1o  9079  indexfi  9272  ixpiunwdom  9507  dfac8clem  9954  acni2  9968  ac6c4  10403  iundom2g  10462  uniimadomf  10467  rabssnn0fi  13921  rlim2  15431  ello1mpt  15456  o1compt  15522  fsum00  15733  iserodd  16775  pcmptdvds  16834  catpropd  17644  invfuc  17913  gsummptnn0fz  19927  gsummoncoe1  22264  gsumply1eq  22265  fiuncmp  23360  elptr2  23530  ptcld  23569  ptclsg  23571  ptcnplem  23577  cnmpt11  23619  cnmpt21  23627  ovoliunlem3  25473  ovoliun  25474  ovoliun2  25475  finiunmbl  25513  volfiniun  25516  iunmbl  25522  voliun  25523  mbfeqalem1  25610  mbfsup  25633  mbfinf  25634  mbflim  25637  itg2split  25718  itgeqa  25783  itgfsum  25796  itgabs  25804  itggt0  25813  limciun  25863  dvlipcn  25967  dvfsumlem4  26004  dvfsum2  26009  itgsubst  26024  coeeq2  26215  ulmss  26374  leibpi  26920  rlimcnp  26943  o1cxp  26953  lgamgulmlem6  27012  fsumdvdscom  27163  lgseisenlem2  27355  disjunsn  32681  bnj110  35034  bnj1529  35246  weiunpo  36681  weiunso  36682  weiunfr  36683  weiunse  36684  poimirlem23  37894  itgabsnc  37940  itggt0cn  37941  totbndbnd  38040  aks6d1c1p5  42482  aks6d1c1rh  42495  aks6d1c7  42554  unitscyglem3  42567  disjinfi  45551  fmptf  45597  caucvgbf  45847  climinff  45971  idlimc  45986  fnlimabslt  46037  limsupref  46043  limsupbnd1f  46044  climbddf  46045  climinf2  46065  limsupubuz  46071  climinfmpt  46073  limsupmnf  46079  limsupre2  46083  limsupmnfuz  46085  limsupre3  46091  limsupre3uz  46094  limsupreuz  46095  climuz  46102  lmbr3  46105  limsupgt  46136  liminfreuz  46161  liminflt  46163  xlimpnfxnegmnf  46172  xlimmnf  46199  xlimpnf  46200  dfxlim2  46206  cncfshift  46232  stoweidlem31  46389  iundjiun  46818  meaiunincf  46841  pimgtmnf2  47072  smfpimcc  47166  smfsup  47172  smfinflem  47175  smfinf  47176  cbvral2  47463