Theorem cbvralw 3276

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-11 2162  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2809  df-nfc 2883  df-ral 3050

This theorem is referenced by:  cbvralsvwOLD  3287  cbvralsvwOLDOLD  3288  cbviin  4989  disjxun  5094  ralxpf  5793  eqfnfv2f  6978  ralrnmptw  7037  dff13f  7199  ofrfval2  7641  fmpox  8009  ovmptss  8033  cbvixp  8850  mptelixpg  8871  boxcutc  8877  xpf1o  9065  indexfi  9258  ixpiunwdom  9493  dfac8clem  9940  acni2  9954  ac6c4  10389  iundom2g  10448  uniimadomf  10453  rabssnn0fi  13907  rlim2  15417  ello1mpt  15442  o1compt  15508  fsum00  15719  iserodd  16761  pcmptdvds  16820  catpropd  17630  invfuc  17899  gsummptnn0fz  19913  gsummoncoe1  22250  gsumply1eq  22251  fiuncmp  23346  elptr2  23516  ptcld  23555  ptclsg  23557  ptcnplem  23563  cnmpt11  23605  cnmpt21  23613  ovoliunlem3  25459  ovoliun  25460  ovoliun2  25461  finiunmbl  25499  volfiniun  25502  iunmbl  25508  voliun  25509  mbfeqalem1  25596  mbfsup  25619  mbfinf  25620  mbflim  25623  itg2split  25704  itgeqa  25769  itgfsum  25782  itgabs  25790  itggt0  25799  limciun  25849  dvlipcn  25953  dvfsumlem4  25990  dvfsum2  25995  itgsubst  26010  coeeq2  26201  ulmss  26360  leibpi  26906  rlimcnp  26929  o1cxp  26939  lgamgulmlem6  26998  fsumdvdscom  27149  lgseisenlem2  27341  disjunsn  32618  bnj110  34963  bnj1529  35175  weiunpo  36608  weiunso  36609  weiunfr  36610  weiunse  36611  poimirlem23  37783  itgabsnc  37829  itggt0cn  37830  totbndbnd  37929  aks6d1c1p5  42305  aks6d1c1rh  42318  aks6d1c7  42377  unitscyglem3  42390  disjinfi  45378  fmptf  45425  caucvgbf  45675  climinff  45799  idlimc  45814  fnlimabslt  45865  limsupref  45871  limsupbnd1f  45872  climbddf  45873  climinf2  45893  limsupubuz  45899  climinfmpt  45901  limsupmnf  45907  limsupre2  45911  limsupmnfuz  45913  limsupre3  45919  limsupre3uz  45922  limsupreuz  45923  climuz  45930  lmbr3  45933  limsupgt  45964  liminfreuz  45989  liminflt  45991  xlimpnfxnegmnf  46000  xlimmnf  46027  xlimpnf  46028  dfxlim2  46034  cncfshift  46060  stoweidlem31  46217  iundjiun  46646  meaiunincf  46669  pimgtmnf2  46900  smfpimcc  46994  smfsup  47000  smfinflem  47003  smfinf  47004  cbvral2  47291