Theorem cbvralw 3363

Description: Rule used to change bound variables, using implicit substitution. Version of cbvral 3368 with a disjoint variable condition, which does not require ax-13 2372. (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 2906	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2906	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3358	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1787  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-clel 2817  df-nfc 2888  df-ral 3068

This theorem is referenced by:  cbvralsvw  3391  cbviin  4963  disjxun  5068  ralxpf  5744  eqfnfv2f  6895  ralrnmptw  6952  dff13f  7110  ofrfval2  7532  fmpox  7880  ovmptss  7904  cbvixp  8660  mptelixpg  8681  boxcutc  8687  xpf1o  8875  indexfi  9057  ixpiunwdom  9279  dfac8clem  9719  acni2  9733  ac6c4  10168  iundom2g  10227  uniimadomf  10232  rabssnn0fi  13634  rlim2  15133  ello1mpt  15158  o1compt  15224  fsum00  15438  iserodd  16464  pcmptdvds  16523  catpropd  17335  invfuc  17608  gsummptnn0fz  19502  gsummoncoe1  21385  gsumply1eq  21386  fiuncmp  22463  elptr2  22633  ptcld  22672  ptclsg  22674  ptcnplem  22680  cnmpt11  22722  cnmpt21  22730  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  finiunmbl  24613  volfiniun  24616  iunmbl  24622  voliun  24623  mbfeqalem1  24710  mbfsup  24733  mbfinf  24734  mbflim  24737  itg2split  24819  itgeqa  24883  itgfsum  24896  itgabs  24904  itggt0  24913  limciun  24963  dvlipcn  25063  dvfsumlem4  25098  dvfsum2  25103  itgsubst  25118  coeeq2  25308  ulmss  25461  leibpi  25997  rlimcnp  26020  o1cxp  26029  lgamgulmlem6  26088  fsumdvdscom  26239  lgseisenlem2  26429  disjunsn  30834  bnj110  32738  bnj1529  32950  poimirlem23  35727  itgabsnc  35773  itggt0cn  35774  totbndbnd  35874  disjinfi  42620  fmptf  42672  climinff  43042  idlimc  43057  fnlimabslt  43110  limsupref  43116  limsupbnd1f  43117  climbddf  43118  climinf2  43138  limsupubuz  43144  climinfmpt  43146  limsupmnf  43152  limsupre2  43156  limsupmnfuz  43158  limsupre3  43164  limsupre3uz  43167  limsupreuz  43168  climuz  43175  lmbr3  43178  limsupgt  43209  liminfreuz  43234  liminflt  43236  xlimpnfxnegmnf  43245  xlimmnf  43272  xlimpnf  43273  dfxlim2  43279  cncfshift  43305  stoweidlem31  43462  iundjiun  43888  meaiunincf  43911  pimgtmnf2  44138  smfpimcc  44228  smfsup  44234  smfinflem  44237  smfinf  44238  cbvral2  44482