Theorem cbvralw 3271

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3269 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 3269	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  3282  cbvralsvwOLDOLD  3283  cbviin  4986  disjxun  5090  ralxpf  5789  eqfnfv2f  6969  ralrnmptw  7028  dff13f  7192  ofrfval2  7634  fmpox  8002  ovmptss  8026  cbvixp  8841  mptelixpg  8862  boxcutc  8868  xpf1o  9056  indexfi  9250  ixpiunwdom  9482  dfac8clem  9926  acni2  9940  ac6c4  10375  iundom2g  10434  uniimadomf  10439  rabssnn0fi  13893  rlim2  15403  ello1mpt  15428  o1compt  15494  fsum00  15705  iserodd  16747  pcmptdvds  16806  catpropd  17615  invfuc  17884  gsummptnn0fz  19865  gsummoncoe1  22193  gsumply1eq  22194  fiuncmp  23289  elptr2  23459  ptcld  23498  ptclsg  23500  ptcnplem  23506  cnmpt11  23548  cnmpt21  23556  ovoliunlem3  25403  ovoliun  25404  ovoliun2  25405  finiunmbl  25443  volfiniun  25446  iunmbl  25452  voliun  25453  mbfeqalem1  25540  mbfsup  25563  mbfinf  25564  mbflim  25567  itg2split  25648  itgeqa  25713  itgfsum  25726  itgabs  25734  itggt0  25743  limciun  25793  dvlipcn  25897  dvfsumlem4  25934  dvfsum2  25939  itgsubst  25954  coeeq2  26145  ulmss  26304  leibpi  26850  rlimcnp  26873  o1cxp  26883  lgamgulmlem6  26942  fsumdvdscom  27093  lgseisenlem2  27285  disjunsn  32538  bnj110  34825  bnj1529  35037  weiunpo  36439  weiunso  36440  weiunfr  36441  weiunse  36442  poimirlem23  37623  itgabsnc  37669  itggt0cn  37670  totbndbnd  37769  aks6d1c1p5  42085  aks6d1c1rh  42098  aks6d1c7  42157  unitscyglem3  42170  disjinfi  45170  fmptf  45217  caucvgbf  45468  climinff  45592  idlimc  45607  fnlimabslt  45660  limsupref  45666  limsupbnd1f  45667  climbddf  45668  climinf2  45688  limsupubuz  45694  climinfmpt  45696  limsupmnf  45702  limsupre2  45706  limsupmnfuz  45708  limsupre3  45714  limsupre3uz  45717  limsupreuz  45718  climuz  45725  lmbr3  45728  limsupgt  45759  liminfreuz  45784  liminflt  45786  xlimpnfxnegmnf  45795  xlimmnf  45822  xlimpnf  45823  dfxlim2  45829  cncfshift  45855  stoweidlem31  46012  iundjiun  46441  meaiunincf  46464  pimgtmnf2  46695  smfpimcc  46789  smfsup  46795  smfinflem  46798  smfinf  46799  cbvral2  47087