Theorem cbvralw 3286

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

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

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 2007  ax-8 2110  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2809  df-nfc 2885  df-ral 3052

This theorem is referenced by:  cbvralsvwOLD  3298  cbvralsvwOLDOLD  3299  cbviin  5013  disjxun  5117  ralxpf  5826  eqfnfv2f  7025  ralrnmptw  7084  dff13f  7248  ofrfval2  7692  fmpox  8066  ovmptss  8092  cbvixp  8928  mptelixpg  8949  boxcutc  8955  xpf1o  9153  indexfi  9372  ixpiunwdom  9604  dfac8clem  10046  acni2  10060  ac6c4  10495  iundom2g  10554  uniimadomf  10559  rabssnn0fi  14004  rlim2  15512  ello1mpt  15537  o1compt  15603  fsum00  15814  iserodd  16855  pcmptdvds  16914  catpropd  17721  invfuc  17990  gsummptnn0fz  19967  gsummoncoe1  22246  gsumply1eq  22247  fiuncmp  23342  elptr2  23512  ptcld  23551  ptclsg  23553  ptcnplem  23559  cnmpt11  23601  cnmpt21  23609  ovoliunlem3  25457  ovoliun  25458  ovoliun2  25459  finiunmbl  25497  volfiniun  25500  iunmbl  25506  voliun  25507  mbfeqalem1  25594  mbfsup  25617  mbfinf  25618  mbflim  25621  itg2split  25702  itgeqa  25767  itgfsum  25780  itgabs  25788  itggt0  25797  limciun  25847  dvlipcn  25951  dvfsumlem4  25988  dvfsum2  25993  itgsubst  26008  coeeq2  26199  ulmss  26358  leibpi  26904  rlimcnp  26927  o1cxp  26937  lgamgulmlem6  26996  fsumdvdscom  27147  lgseisenlem2  27339  disjunsn  32575  bnj110  34889  bnj1529  35101  weiunpo  36483  weiunso  36484  weiunfr  36485  weiunse  36486  poimirlem23  37667  itgabsnc  37713  itggt0cn  37714  totbndbnd  37813  aks6d1c1p5  42125  aks6d1c1rh  42138  aks6d1c7  42197  unitscyglem3  42210  disjinfi  45216  fmptf  45263  caucvgbf  45516  climinff  45640  idlimc  45655  fnlimabslt  45708  limsupref  45714  limsupbnd1f  45715  climbddf  45716  climinf2  45736  limsupubuz  45742  climinfmpt  45744  limsupmnf  45750  limsupre2  45754  limsupmnfuz  45756  limsupre3  45762  limsupre3uz  45765  limsupreuz  45766  climuz  45773  lmbr3  45776  limsupgt  45807  liminfreuz  45832  liminflt  45834  xlimpnfxnegmnf  45843  xlimmnf  45870  xlimpnf  45871  dfxlim2  45877  cncfshift  45903  stoweidlem31  46060  iundjiun  46489  meaiunincf  46512  pimgtmnf2  46743  smfpimcc  46837  smfsup  46843  smfinflem  46846  smfinf  46847  cbvral2  47132