Theorem cbvralw 3441

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

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1784  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-10 2145  ax-11 2161  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-sb 2070  df-clel 2893  df-nfc 2963  df-ral 3143

This theorem is referenced by:  cbvralsvw  3467  cbviin  4962  disjxun  5064  ralxpf  5717  eqfnfv2f  6806  ralrnmptw  6860  dff13f  7014  ofrfval2  7427  fmpox  7765  ovmptss  7788  cbvixp  8478  mptelixpg  8499  boxcutc  8505  xpf1o  8679  indexfi  8832  ixpiunwdom  9055  dfac8clem  9458  acni2  9472  ac6c4  9903  iundom2g  9962  uniimadomf  9967  rabssnn0fi  13355  rlim2  14853  ello1mpt  14878  o1compt  14944  fsum00  15153  iserodd  16172  pcmptdvds  16230  catpropd  16979  invfuc  17244  gsummptnn0fz  19106  gsummoncoe1  20472  gsumply1eq  20473  fiuncmp  22012  elptr2  22182  ptcld  22221  ptclsg  22223  ptcnplem  22229  cnmpt11  22271  cnmpt21  22279  ovoliunlem3  24105  ovoliun  24106  ovoliun2  24107  finiunmbl  24145  volfiniun  24148  iunmbl  24154  voliun  24155  mbfeqalem1  24242  mbfsup  24265  mbfinf  24266  mbflim  24269  itg2split  24350  itgeqa  24414  itgfsum  24427  itgabs  24435  itggt0  24442  limciun  24492  dvlipcn  24591  dvfsumlem4  24626  dvfsum2  24631  itgsubst  24646  coeeq2  24832  ulmss  24985  leibpi  25520  rlimcnp  25543  o1cxp  25552  lgamgulmlem6  25611  fsumdvdscom  25762  lgseisenlem2  25952  disjunsn  30344  bnj110  32130  bnj1529  32342  poimirlem23  34930  itgabsnc  34976  itggt0cn  34979  totbndbnd  35082  disjinfi  41503  fmptf  41558  climinff  41941  idlimc  41956  fnlimabslt  42009  limsupref  42015  limsupbnd1f  42016  climbddf  42017  climinf2  42037  limsupubuz  42043  climinfmpt  42045  limsupmnf  42051  limsupre2  42055  limsupmnfuz  42057  limsupre3  42063  limsupre3uz  42066  limsupreuz  42067  climuz  42074  lmbr3  42077  limsupgt  42108  liminfreuz  42133  liminflt  42135  xlimpnfxnegmnf  42144  xlimmnf  42171  xlimpnf  42172  dfxlim2  42178  cncfshift  42206  stoweidlem31  42365  iundjiun  42791  meaiunincf  42814  pimgtmnf2  43041  smfpimcc  43131  smfsup  43137  smfinflem  43140  smfinf  43141