Theorem cbvralw 3307

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1813  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-11 2192  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-clel 2838  df-nfc 2912  df-ral 3080

This theorem is referenced by:  cbvralsvwOLD  3318  cbviin  5000  disjxun  5107  ralxpf  5832  eqfnfv2f  7029  ralrnmptw  7089  dff13f  7253  ofrfval2  7695  fmpox  8060  ovmptss  8084  cbvixp  8908  mptelixpg  8929  boxcutc  8935  xpf1o  9123  indexfi  9313  ixpiunwdom  9548  dfac8clem  10012  acni2  10026  ac6c4  10460  iundom2g  10519  uniimadomf  10524  rabssnn0fi  14018  rlim2  15543  ello1mpt  15568  o1compt  15634  fsum00  15846  iserodd  16890  pcmptdvds  16949  catpropd  17760  invfuc  18029  gsummptnn0fz  20051  gsummoncoe1  22468  gsumply1eq  22469  fiuncmp  23561  elptr2  23731  ptcld  23770  ptclsg  23772  ptcnplem  23778  cnmpt11  23820  cnmpt21  23828  ovoliunlem3  25663  ovoliun  25664  ovoliun2  25665  finiunmbl  25703  volfiniun  25706  iunmbl  25712  voliun  25713  mbfeqalem1  25800  mbfsup  25823  mbfinf  25824  mbflim  25827  itg2split  25908  itgeqa  25973  itgfsum  25986  itgabs  25994  itggt0  26003  limciun  26053  dvlipcn  26153  dvfsumlem4  26188  dvfsum2  26193  itgsubst  26208  coeeq2  26399  ulmss  26560  leibpi  27107  rlimcnp  27130  o1cxp  27139  lgamgulmlem6  27198  fsumdvdscom  27349  lgseisenlem2  27540  disjunsn  32939  bnj110  35246  bnj1529  35458  weiunpo  36976  weiunso  36977  weiunfr  36978  weiunse  36979  poimirlem23  38294  itgabsnc  38340  itggt0cn  38341  totbndbnd  38440  aks6d1c1p5  42879  aks6d1c1rh  42892  aks6d1c7  42951  unitscyglem3  42964  disjinfi  45910  fmptf  45954  caucvgbf  46203  climinff  46327  idlimc  46342  fnlimabslt  46393  limsupref  46399  limsupbnd1f  46400  climbddf  46401  climinf2  46421  limsupubuz  46427  climinfmpt  46429  limsupmnf  46435  limsupre2  46439  limsupmnfuz  46441  limsupre3  46447  limsupre3uz  46450  limsupreuz  46451  climuz  46458  lmbr3  46461  limsupgt  46492  liminfreuz  46517  liminflt  46519  xlimpnfxnegmnf  46528  xlimmnf  46555  xlimpnf  46556  dfxlim2  46562  cncfshift  46588  stoweidlem31  46745  iundjiun  47174  meaiunincf  47197  pimgtmnf2  47428  smfpimcc  47522  smfsup  47528  smfinflem  47531  smfinf  47532  cbvral2  47840