Theorem cbvralw 3278

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045

This theorem is referenced by:  cbvralsvwOLD  3289  cbvralsvwOLDOLD  3290  cbviin  4996  disjxun  5100  ralxpf  5800  eqfnfv2f  6989  ralrnmptw  7048  dff13f  7212  ofrfval2  7654  fmpox  8025  ovmptss  8049  cbvixp  8864  mptelixpg  8885  boxcutc  8891  xpf1o  9080  indexfi  9287  ixpiunwdom  9519  dfac8clem  9961  acni2  9975  ac6c4  10410  iundom2g  10469  uniimadomf  10474  rabssnn0fi  13927  rlim2  15438  ello1mpt  15463  o1compt  15529  fsum00  15740  iserodd  16782  pcmptdvds  16841  catpropd  17650  invfuc  17919  gsummptnn0fz  19900  gsummoncoe1  22228  gsumply1eq  22229  fiuncmp  23324  elptr2  23494  ptcld  23533  ptclsg  23535  ptcnplem  23541  cnmpt11  23583  cnmpt21  23591  ovoliunlem3  25438  ovoliun  25439  ovoliun2  25440  finiunmbl  25478  volfiniun  25481  iunmbl  25487  voliun  25488  mbfeqalem1  25575  mbfsup  25598  mbfinf  25599  mbflim  25602  itg2split  25683  itgeqa  25748  itgfsum  25761  itgabs  25769  itggt0  25778  limciun  25828  dvlipcn  25932  dvfsumlem4  25969  dvfsum2  25974  itgsubst  25989  coeeq2  26180  ulmss  26339  leibpi  26885  rlimcnp  26908  o1cxp  26918  lgamgulmlem6  26977  fsumdvdscom  27128  lgseisenlem2  27320  disjunsn  32573  bnj110  34841  bnj1529  35053  weiunpo  36446  weiunso  36447  weiunfr  36448  weiunse  36449  poimirlem23  37630  itgabsnc  37676  itggt0cn  37677  totbndbnd  37776  aks6d1c1p5  42093  aks6d1c1rh  42106  aks6d1c7  42165  unitscyglem3  42178  disjinfi  45179  fmptf  45226  caucvgbf  45478  climinff  45602  idlimc  45617  fnlimabslt  45670  limsupref  45676  limsupbnd1f  45677  climbddf  45678  climinf2  45698  limsupubuz  45704  climinfmpt  45706  limsupmnf  45712  limsupre2  45716  limsupmnfuz  45718  limsupre3  45724  limsupre3uz  45727  limsupreuz  45728  climuz  45735  lmbr3  45738  limsupgt  45769  liminfreuz  45794  liminflt  45796  xlimpnfxnegmnf  45805  xlimmnf  45832  xlimpnf  45833  dfxlim2  45839  cncfshift  45865  stoweidlem31  46022  iundjiun  46451  meaiunincf  46474  pimgtmnf2  46705  smfpimcc  46799  smfsup  46805  smfinflem  46808  smfinf  46809  cbvral2  47097