Theorem cbvralw 3306

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

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

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 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2837  df-nfc 2911  df-ral 3079

This theorem is used by:  cbviin  4998  disjxun  5105  ralxpf  5830  eqfnfv2f  7030  ralrnmptw  7091  dff13f  7256  ofrfval2  7703  fmpox  8068  ovmptss  8094  cbvixp  8925  mptelixpg  8946  boxcutc  8952  xpf1o  9141  indexfi  9331  ixpiunwdom  9566  dfac8clem  10039  acni2  10053  ac6c4  10487  iundom2g  10552  uniimadomf  10557  rabssnn0fi  14054  rlim2  15587  ello1mpt  15612  o1compt  15678  fsum00  15889  iserodd  16933  pcmptdvds  16992  catpropd  17803  invfuc  18072  gsummptnn0fz  20119  gsummoncoe1  22539  gsumply1eq  22540  fiuncmp  23635  elptr2  23806  ptcld  23845  ptclsg  23847  ptcnplem  23853  cnmpt11  23895  cnmpt21  23903  ovoliunlem3  25738  ovoliun  25739  ovoliun2  25740  finiunmbl  25778  volfiniun  25781  iunmbl  25787  voliun  25788  mbfeqalem1  25875  mbfsup  25898  mbfinf  25899  mbflim  25902  itg2split  25983  itgeqa  26048  itgfsum  26061  itgabs  26069  itggt0  26078  limciun  26128  dvlipcn  26228  dvfsumlem4  26263  dvfsum2  26268  itgsubst  26283  coeeq2  26475  ulmss  26640  leibpi  27187  rlimcnp  27210  o1cxp  27219  lgamgulmlem6  27278  fsumdvdscom  27429  lgseisenlem2  27620  disjunsn  33075  bnj110  35375  bnj1529  35587  weiunpo  37092  weiunso  37093  weiunfr  37094  weiunse  37095  poimirlem23  38400  itgabsnc  38446  itggt0cn  38447  totbndbnd  38547  aks6d1c1p5  42986  aks6d1c1rh  42999  aks6d1c7  43058  unitscyglem3  43071  disjinfi  46032  fmptf  46076  caucvgbf  46325  climinff  46449  idlimc  46464  fnlimabslt  46515  limsupref  46521  limsupbnd1f  46522  climbddf  46523  climinf2  46543  limsupubuz  46549  climinfmpt  46551  limsupmnf  46557  limsupre2  46561  limsupmnfuz  46563  limsupre3  46569  limsupre3uz  46572  limsupreuz  46573  climuz  46580  lmbr3  46583  limsupgt  46614  liminfreuz  46639  liminflt  46641  xlimpnfxnegmnf  46650  xlimmnf  46677  xlimpnf  46678  dfxlim2  46684  cncfshift  46710  stoweidlem31  46867  iundjiun  47296  meaiunincf  47319  pimgtmnf2  47550  smfpimcc  47644  smfsup  47650  smfinflem  47653  smfinf  47654  cbvral2  47999