Theorem cbvralw 3304

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-11 2193  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-clel 2835  df-nfc 2909  df-ral 3077

This theorem is used by:  cbviin  4993  disjxun  5100  ralxpf  5825  eqfnfv2f  7038  ralrnmptw  7099  dff13f  7263  ofrfval2  7718  fmpox  8083  ovmptssOLD  8110  cbvixp  8950  mptelixpg  8971  boxcutc  8977  xpf1o  9166  indexfi  9357  ixpiunwdom  9591  dfac8clem  10118  acni2  10132  ac6c4  10566  iundom2g  10631  uniimadomf  10636  rabssnn0fi  14136  rlim2  15672  ello1mpt  15697  o1compt  15763  fsum00  15974  iserodd  17022  pcmptdvds  17081  catpropd  17892  invfuc  18161  gsummptnn0fz  20209  gsummoncoe1  22635  gsumply1eq  22636  fiuncmp  23731  elptr2  23902  ptcld  23941  ptclsg  23943  ptcnplem  23949  cnmpt11  23991  cnmpt21  23999  ovoliunlem3  25834  ovoliun  25835  ovoliun2  25836  finiunmbl  25874  volfiniun  25877  iunmbl  25883  voliun  25884  mbfeqalem1  25971  mbfsup  25994  mbfinf  25995  mbflim  25998  itg2split  26079  itgeqa  26143  itgfsum  26156  itgabs  26164  itggt0  26173  limciun  26223  dvlipcn  26323  dvfsumlem4  26358  dvfsum2  26363  itgsubst  26378  coeeq2  26570  ulmss  26733  leibpi  27279  rlimcnp  27302  o1cxp  27311  lgamgulmlem6  27370  fsumdvdscom  27521  lgseisenlem2  27712  disjunsn  33239  bnj110  35538  bnj1529  35750  rankse  35799  weiunpo  37377  weiunso  37378  weiunfr  37379  weiunse  37380  poimirlem23  38698  itgabsnc  38744  itggt0cn  38745  totbndbnd  38860  aks6d1c1p5  43299  aks6d1c1rh  43312  aks6d1c7  43371  unitscyglem3  43384  disjinfi  46343  fmptf  46387  caucvgbf  46635  climinff  46759  idlimc  46774  fnlimabslt  46825  limsupref  46831  limsupbnd1f  46832  climbddf  46833  climinf2  46853  limsupubuz  46859  climinfmpt  46861  limsupmnf  46867  limsupre2  46871  limsupmnfuz  46873  limsupre3  46879  limsupre3uz  46882  limsupreuz  46883  climuz  46890  lmbr3  46893  limsupgt  46924  liminfreuz  46949  liminflt  46951  xlimpnfxnegmnf  46960  xlimmnf  46987  xlimpnf  46988  dfxlim2  46994  cncfshift  47020  stoweidlem31  47177  iundjiun  47606  meaiunincf  47629  pimgtmnf2  47860  smfpimcc  47954  smfsup  47960  smfinflem  47963  smfinf  47964  cbvral2  48310