Theorem cbvralw 3387

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1785  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-11 2158  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-clel 2870  df-nfc 2938  df-ral 3111

This theorem is referenced by:  cbvralsvw  3414  cbviin  4924  disjxun  5028  ralxpf  5681  eqfnfv2f  6783  ralrnmptw  6837  dff13f  6992  ofrfval2  7407  fmpox  7747  ovmptss  7771  cbvixp  8461  mptelixpg  8482  boxcutc  8488  xpf1o  8663  indexfi  8816  ixpiunwdom  9038  dfac8clem  9443  acni2  9457  ac6c4  9892  iundom2g  9951  uniimadomf  9956  rabssnn0fi  13349  rlim2  14845  ello1mpt  14870  o1compt  14936  fsum00  15145  iserodd  16162  pcmptdvds  16220  catpropd  16971  invfuc  17236  gsummptnn0fz  19099  gsummoncoe1  20933  gsumply1eq  20934  fiuncmp  22009  elptr2  22179  ptcld  22218  ptclsg  22220  ptcnplem  22226  cnmpt11  22268  cnmpt21  22276  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  finiunmbl  24148  volfiniun  24151  iunmbl  24157  voliun  24158  mbfeqalem1  24245  mbfsup  24268  mbfinf  24269  mbflim  24272  itg2split  24353  itgeqa  24417  itgfsum  24430  itgabs  24438  itggt0  24447  limciun  24497  dvlipcn  24597  dvfsumlem4  24632  dvfsum2  24637  itgsubst  24652  coeeq2  24839  ulmss  24992  leibpi  25528  rlimcnp  25551  o1cxp  25560  lgamgulmlem6  25619  fsumdvdscom  25770  lgseisenlem2  25960  disjunsn  30357  bnj110  32240  bnj1529  32452  poimirlem23  35080  itgabsnc  35126  itggt0cn  35127  totbndbnd  35227  disjinfi  41820  fmptf  41875  climinff  42253  idlimc  42268  fnlimabslt  42321  limsupref  42327  limsupbnd1f  42328  climbddf  42329  climinf2  42349  limsupubuz  42355  climinfmpt  42357  limsupmnf  42363  limsupre2  42367  limsupmnfuz  42369  limsupre3  42375  limsupre3uz  42378  limsupreuz  42379  climuz  42386  lmbr3  42389  limsupgt  42420  liminfreuz  42445  liminflt  42447  xlimpnfxnegmnf  42456  xlimmnf  42483  xlimpnf  42484  dfxlim2  42490  cncfshift  42516  stoweidlem31  42673  iundjiun  43099  meaiunincf  43122  pimgtmnf2  43349  smfpimcc  43439  smfsup  43445  smfinflem  43448  smfinf  43449  cbvral2  43658