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  17646  invfuc  17915  gsummptnn0fz  19892  gsummoncoe1  22171  gsumply1eq  22172  fiuncmp  23267  elptr2  23437  ptcld  23476  ptclsg  23478  ptcnplem  23484  cnmpt11  23526  cnmpt21  23534  ovoliunlem3  25381  ovoliun  25382  ovoliun2  25383  finiunmbl  25421  volfiniun  25424  iunmbl  25430  voliun  25431  mbfeqalem1  25518  mbfsup  25541  mbfinf  25542  mbflim  25545  itg2split  25626  itgeqa  25691  itgfsum  25704  itgabs  25712  itggt0  25721  limciun  25771  dvlipcn  25875  dvfsumlem4  25912  dvfsum2  25917  itgsubst  25932  coeeq2  26123  ulmss  26282  leibpi  26828  rlimcnp  26851  o1cxp  26861  lgamgulmlem6  26920  fsumdvdscom  27071  lgseisenlem2  27263  disjunsn  32496  bnj110  34821  bnj1529  35033  weiunpo  36426  weiunso  36427  weiunfr  36428  weiunse  36429  poimirlem23  37610  itgabsnc  37656  itggt0cn  37657  totbndbnd  37756  aks6d1c1p5  42073  aks6d1c1rh  42086  aks6d1c7  42145  unitscyglem3  42158  disjinfi  45159  fmptf  45206  caucvgbf  45458  climinff  45582  idlimc  45597  fnlimabslt  45650  limsupref  45656  limsupbnd1f  45657  climbddf  45658  climinf2  45678  limsupubuz  45684  climinfmpt  45686  limsupmnf  45692  limsupre2  45696  limsupmnfuz  45698  limsupre3  45704  limsupre3uz  45707  limsupreuz  45708  climuz  45715  lmbr3  45718  limsupgt  45749  liminfreuz  45774  liminflt  45776  xlimpnfxnegmnf  45785  xlimmnf  45812  xlimpnf  45813  dfxlim2  45819  cncfshift  45845  stoweidlem31  46002  iundjiun  46431  meaiunincf  46454  pimgtmnf2  46685  smfpimcc  46779  smfsup  46785  smfinflem  46788  smfinf  46789  cbvral2  47077