Theorem cbvralw 3313

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1810  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-11 2198  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-clel 2844  df-nfc 2918  df-ral 3086

This theorem is referenced by:  cbvralsvwOLD  3324  cbviin  5004  disjxun  5111  ralxpf  5833  eqfnfv2f  7030  ralrnmptw  7090  dff13f  7254  ofrfval2  7696  fmpox  8063  ovmptss  8087  cbvixp  8911  mptelixpg  8932  boxcutc  8938  xpf1o  9126  indexfi  9316  ixpiunwdom  9551  dfac8clem  10015  acni2  10029  ac6c4  10464  iundom2g  10523  uniimadomf  10528  rabssnn0fi  14021  rlim2  15546  ello1mpt  15571  o1compt  15637  fsum00  15849  iserodd  16894  pcmptdvds  16953  catpropd  17764  invfuc  18033  gsummptnn0fz  20055  gsummoncoe1  22436  gsumply1eq  22437  fiuncmp  23529  elptr2  23699  ptcld  23738  ptclsg  23740  ptcnplem  23746  cnmpt11  23788  cnmpt21  23796  ovoliunlem3  25631  ovoliun  25632  ovoliun2  25633  finiunmbl  25671  volfiniun  25674  iunmbl  25680  voliun  25681  mbfeqalem1  25768  mbfsup  25791  mbfinf  25792  mbflim  25795  itg2split  25876  itgeqa  25941  itgfsum  25954  itgabs  25962  itggt0  25971  limciun  26021  dvlipcn  26121  dvfsumlem4  26156  dvfsum2  26161  itgsubst  26176  coeeq2  26367  ulmss  26525  leibpi  27072  rlimcnp  27095  o1cxp  27104  lgamgulmlem6  27163  fsumdvdscom  27314  lgseisenlem2  27505  disjunsn  32879  bnj110  35190  bnj1529  35402  weiunpo  36864  weiunso  36865  weiunfr  36866  weiunse  36867  poimirlem23  38181  itgabsnc  38227  itggt0cn  38228  totbndbnd  38327  aks6d1c1p5  42768  aks6d1c1rh  42781  aks6d1c7  42840  unitscyglem3  42853  disjinfi  45801  fmptf  45845  caucvgbf  46094  climinff  46218  idlimc  46233  fnlimabslt  46284  limsupref  46290  limsupbnd1f  46291  climbddf  46292  climinf2  46312  limsupubuz  46318  climinfmpt  46320  limsupmnf  46326  limsupre2  46330  limsupmnfuz  46332  limsupre3  46338  limsupre3uz  46341  limsupreuz  46342  climuz  46349  lmbr3  46352  limsupgt  46383  liminfreuz  46408  liminflt  46410  xlimpnfxnegmnf  46419  xlimmnf  46446  xlimpnf  46447  dfxlim2  46453  cncfshift  46479  stoweidlem31  46636  iundjiun  47065  meaiunincf  47088  pimgtmnf2  47319  smfpimcc  47413  smfsup  47419  smfinflem  47422  smfinf  47423  cbvral2  47728