Theorem cbvralw 3312

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1781  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-clel 2819  df-nfc 2895  df-ral 3068

This theorem is referenced by:  cbvralsvwOLD  3325  cbvralsvwOLDOLD  3326  cbviin  5060  disjxun  5164  ralxpf  5871  eqfnfv2f  7068  ralrnmptw  7128  dff13f  7293  ofrfval2  7735  fmpox  8108  ovmptss  8134  cbvixp  8972  mptelixpg  8993  boxcutc  8999  xpf1o  9205  indexfi  9430  ixpiunwdom  9659  dfac8clem  10101  acni2  10115  ac6c4  10550  iundom2g  10609  uniimadomf  10614  rabssnn0fi  14037  rlim2  15542  ello1mpt  15567  o1compt  15633  fsum00  15846  iserodd  16882  pcmptdvds  16941  catpropd  17767  invfuc  18044  gsummptnn0fz  20028  gsummoncoe1  22333  gsumply1eq  22334  fiuncmp  23433  elptr2  23603  ptcld  23642  ptclsg  23644  ptcnplem  23650  cnmpt11  23692  cnmpt21  23700  ovoliunlem3  25558  ovoliun  25559  ovoliun2  25560  finiunmbl  25598  volfiniun  25601  iunmbl  25607  voliun  25608  mbfeqalem1  25695  mbfsup  25718  mbfinf  25719  mbflim  25722  itg2split  25804  itgeqa  25869  itgfsum  25882  itgabs  25890  itggt0  25899  limciun  25949  dvlipcn  26053  dvfsumlem4  26090  dvfsum2  26095  itgsubst  26110  coeeq2  26301  ulmss  26458  leibpi  27003  rlimcnp  27026  o1cxp  27036  lgamgulmlem6  27095  fsumdvdscom  27246  lgseisenlem2  27438  disjunsn  32616  bnj110  34834  bnj1529  35046  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  poimirlem23  37603  itgabsnc  37649  itggt0cn  37650  totbndbnd  37749  aks6d1c1p5  42069  aks6d1c1rh  42082  aks6d1c7  42141  unitscyglem3  42154  disjinfi  45099  fmptf  45147  caucvgbf  45405  climinff  45532  idlimc  45547  fnlimabslt  45600  limsupref  45606  limsupbnd1f  45607  climbddf  45608  climinf2  45628  limsupubuz  45634  climinfmpt  45636  limsupmnf  45642  limsupre2  45646  limsupmnfuz  45648  limsupre3  45654  limsupre3uz  45657  limsupreuz  45658  climuz  45665  lmbr3  45668  limsupgt  45699  liminfreuz  45724  liminflt  45726  xlimpnfxnegmnf  45735  xlimmnf  45762  xlimpnf  45763  dfxlim2  45769  cncfshift  45795  stoweidlem31  45952  iundjiun  46381  meaiunincf  46404  pimgtmnf2  46635  smfpimcc  46729  smfsup  46735  smfinflem  46738  smfinf  46739  cbvral2  47018