Theorem cbvralw 3308

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3306 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 2926	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2926	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2839  df-nfc 2913  df-ral 3081

This theorem is used by:  cbviin  4999  disjxun  5106  ralxpf  5834  eqfnfv2f  7064  ralrnmptw  7126  dff13f  7290  ofrfval2  7746  fmpox  8113  ovmptssOLD  8140  cbvixp  8980  mptelixpg  9001  boxcutc  9007  xpf1o  9196  indexfi  9387  ixpiunwdom  9621  dfac8clem  10150  acni2  10164  ac6c4  10598  iundom2g  10663  uniimadomf  10668  rabssnn0fi  14169  rlim2  15707  ello1mpt  15732  o1compt  15798  fsum00  16009  iserodd  17057  pcmptdvds  17116  catpropd  17933  invfuc  18202  gsummptnn0fz  20251  gsummoncoe1  22681  gsumply1eq  22682  fiuncmp  23777  elptr2  23948  ptcld  23987  ptclsg  23989  ptcnplem  23995  cnmpt11  24037  cnmpt21  24045  ovoliunlem3  25880  ovoliun  25881  ovoliun2  25882  finiunmbl  25920  volfiniun  25923  iunmbl  25929  voliun  25930  mbfeqalem1  26017  mbfsup  26040  mbfinf  26041  mbflim  26044  itg2split  26125  itgeqa  26189  itgfsum  26202  itgabs  26210  itggt0  26219  limciun  26269  dvlipcn  26369  dvfsumlem4  26404  dvfsum2  26409  itgsubst  26424  coeeq2  26616  ulmss  26781  leibpi  27327  rlimcnp  27350  o1cxp  27359  lgamgulmlem6  27418  fsumdvdscom  27569  lgseisenlem2  27760  disjunsn  33286  bnj110  35599  bnj1529  35811  rankse  35864  weiunpo  37468  weiunso  37469  weiunfr  37470  weiunse  37471  poimirlem23  38829  itgabsnc  38875  itggt0cn  38876  totbndbnd  38989  aks6d1c1p5  43428  aks6d1c1rh  43441  aks6d1c7  43500  unitscyglem3  43513  disjinfi  46480  fmptf  46524  caucvgbf  46772  climinff  46896  idlimc  46911  fnlimabslt  46962  limsupref  46968  limsupbnd1f  46969  climbddf  46970  climinf2  46990  limsupubuz  46996  climinfmpt  46998  limsupmnf  47004  limsupre2  47008  limsupmnfuz  47010  limsupre3  47016  limsupre3uz  47019  limsupreuz  47020  climuz  47027  lmbr3  47030  limsupgt  47061  liminfreuz  47086  liminflt  47088  xlimpnfxnegmnf  47097  xlimmnf  47124  xlimpnf  47125  dfxlim2  47131  cncfshift  47157  stoweidlem31  47314  iundjiun  47743  meaiunincf  47766  pimgtmnf2  47997  smfpimcc  48091  smfsup  48097  smfinflem  48100  smfinf  48101  cbvral2  48447