Theorem cbvralw 3305

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2836  df-nfc 2910  df-ral 3078

This theorem is used by:  cbviin  4994  disjxun  5101  ralxpf  5824  eqfnfv2f  7031  ralrnmptw  7092  dff13f  7257  ofrfval2  7712  fmpox  8076  ovmptss  8102  cbvixp  8935  mptelixpg  8956  boxcutc  8962  xpf1o  9151  indexfi  9342  ixpiunwdom  9577  dfac8clem  10104  acni2  10118  ac6c4  10552  iundom2g  10617  uniimadomf  10622  rabssnn0fi  14122  rlim2  15656  ello1mpt  15681  o1compt  15747  fsum00  15958  iserodd  17006  pcmptdvds  17065  catpropd  17876  invfuc  18145  gsummptnn0fz  20193  gsummoncoe1  22619  gsumply1eq  22620  fiuncmp  23715  elptr2  23886  ptcld  23925  ptclsg  23927  ptcnplem  23933  cnmpt11  23975  cnmpt21  23983  ovoliunlem3  25818  ovoliun  25819  ovoliun2  25820  finiunmbl  25858  volfiniun  25861  iunmbl  25867  voliun  25868  mbfeqalem1  25955  mbfsup  25978  mbfinf  25979  mbflim  25982  itg2split  26063  itgeqa  26127  itgfsum  26140  itgabs  26148  itggt0  26157  limciun  26207  dvlipcn  26307  dvfsumlem4  26342  dvfsum2  26347  itgsubst  26362  coeeq2  26554  ulmss  26717  leibpi  27263  rlimcnp  27286  o1cxp  27295  lgamgulmlem6  27354  fsumdvdscom  27505  lgseisenlem2  27696  disjunsn  33181  bnj110  35481  bnj1529  35693  weiunpo  37233  weiunso  37234  weiunfr  37235  weiunse  37236  poimirlem23  38541  itgabsnc  38587  itggt0cn  38588  totbndbnd  38703  aks6d1c1p5  43142  aks6d1c1rh  43155  aks6d1c7  43214  unitscyglem3  43227  disjinfi  46176  fmptf  46220  caucvgbf  46468  climinff  46592  idlimc  46607  fnlimabslt  46658  limsupref  46664  limsupbnd1f  46665  climbddf  46666  climinf2  46686  limsupubuz  46692  climinfmpt  46694  limsupmnf  46700  limsupre2  46704  limsupmnfuz  46706  limsupre3  46712  limsupre3uz  46715  limsupreuz  46716  climuz  46723  lmbr3  46726  limsupgt  46757  liminfreuz  46782  liminflt  46784  xlimpnfxnegmnf  46793  xlimmnf  46820  xlimpnf  46821  dfxlim2  46827  cncfshift  46853  stoweidlem31  47010  iundjiun  47439  meaiunincf  47462  pimgtmnf2  47693  smfpimcc  47787  smfsup  47793  smfinflem  47796  smfinf  47797  cbvral2  48142