Theorem cbvralw 3374

Description: Rule used to change bound variables, using implicit substitution. Version of cbvral 3380 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 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 2908	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2908	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3369	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1786  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-11 2155  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-clel 2817  df-nfc 2890  df-ral 3070

This theorem is referenced by:  cbvralsvw  3403  cbviin  4968  disjxun  5073  ralxpf  5758  eqfnfv2f  6922  ralrnmptw  6979  dff13f  7138  ofrfval2  7563  fmpox  7916  ovmptss  7942  cbvixp  8711  mptelixpg  8732  boxcutc  8738  xpf1o  8935  indexfi  9136  ixpiunwdom  9358  dfac8clem  9797  acni2  9811  ac6c4  10246  iundom2g  10305  uniimadomf  10310  rabssnn0fi  13715  rlim2  15214  ello1mpt  15239  o1compt  15305  fsum00  15519  iserodd  16545  pcmptdvds  16604  catpropd  17427  invfuc  17701  gsummptnn0fz  19596  gsummoncoe1  21484  gsumply1eq  21485  fiuncmp  22564  elptr2  22734  ptcld  22773  ptclsg  22775  ptcnplem  22781  cnmpt11  22823  cnmpt21  22831  ovoliunlem3  24677  ovoliun  24678  ovoliun2  24679  finiunmbl  24717  volfiniun  24720  iunmbl  24726  voliun  24727  mbfeqalem1  24814  mbfsup  24837  mbfinf  24838  mbflim  24841  itg2split  24923  itgeqa  24987  itgfsum  25000  itgabs  25008  itggt0  25017  limciun  25067  dvlipcn  25167  dvfsumlem4  25202  dvfsum2  25207  itgsubst  25222  coeeq2  25412  ulmss  25565  leibpi  26101  rlimcnp  26124  o1cxp  26133  lgamgulmlem6  26192  fsumdvdscom  26343  lgseisenlem2  26533  disjunsn  30942  bnj110  32847  bnj1529  33059  poimirlem23  35809  itgabsnc  35855  itggt0cn  35856  totbndbnd  35956  disjinfi  42738  fmptf  42790  climinff  43159  idlimc  43174  fnlimabslt  43227  limsupref  43233  limsupbnd1f  43234  climbddf  43235  climinf2  43255  limsupubuz  43261  climinfmpt  43263  limsupmnf  43269  limsupre2  43273  limsupmnfuz  43275  limsupre3  43281  limsupre3uz  43284  limsupreuz  43285  climuz  43292  lmbr3  43295  limsupgt  43326  liminfreuz  43351  liminflt  43353  xlimpnfxnegmnf  43362  xlimmnf  43389  xlimpnf  43390  dfxlim2  43396  cncfshift  43422  stoweidlem31  43579  iundjiun  44005  meaiunincf  44028  pimgtmnf2  44259  smfpimcc  44352  smfsup  44358  smfinflem  44361  smfinf  44362  cbvral2  44606