Theorem cbvralw 3340

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1790  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-11 2162  ax-12 2179

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-nf 1791  df-clel 2811  df-nfc 2881  df-ral 3058

This theorem is referenced by:  cbvralsvw  3368  cbviin  4923  disjxun  5028  ralxpf  5689  eqfnfv2f  6813  ralrnmptw  6870  dff13f  7025  ofrfval2  7445  fmpox  7790  ovmptss  7814  cbvixp  8524  mptelixpg  8545  boxcutc  8551  xpf1o  8729  indexfi  8905  ixpiunwdom  9127  dfac8clem  9532  acni2  9546  ac6c4  9981  iundom2g  10040  uniimadomf  10045  rabssnn0fi  13445  rlim2  14943  ello1mpt  14968  o1compt  15034  fsum00  15246  iserodd  16272  pcmptdvds  16330  catpropd  17083  invfuc  17349  gsummptnn0fz  19225  gsummoncoe1  21079  gsumply1eq  21080  fiuncmp  22155  elptr2  22325  ptcld  22364  ptclsg  22366  ptcnplem  22372  cnmpt11  22414  cnmpt21  22422  ovoliunlem3  24256  ovoliun  24257  ovoliun2  24258  finiunmbl  24296  volfiniun  24299  iunmbl  24305  voliun  24306  mbfeqalem1  24393  mbfsup  24416  mbfinf  24417  mbflim  24420  itg2split  24502  itgeqa  24566  itgfsum  24579  itgabs  24587  itggt0  24596  limciun  24646  dvlipcn  24746  dvfsumlem4  24781  dvfsum2  24786  itgsubst  24801  coeeq2  24991  ulmss  25144  leibpi  25680  rlimcnp  25703  o1cxp  25712  lgamgulmlem6  25771  fsumdvdscom  25922  lgseisenlem2  26112  disjunsn  30507  bnj110  32409  bnj1529  32621  poimirlem23  35423  itgabsnc  35469  itggt0cn  35470  totbndbnd  35570  disjinfi  42269  fmptf  42320  climinff  42694  idlimc  42709  fnlimabslt  42762  limsupref  42768  limsupbnd1f  42769  climbddf  42770  climinf2  42790  limsupubuz  42796  climinfmpt  42798  limsupmnf  42804  limsupre2  42808  limsupmnfuz  42810  limsupre3  42816  limsupre3uz  42819  limsupreuz  42820  climuz  42827  lmbr3  42830  limsupgt  42861  liminfreuz  42886  liminflt  42888  xlimpnfxnegmnf  42897  xlimmnf  42924  xlimpnf  42925  dfxlim2  42931  cncfshift  42957  stoweidlem31  43114  iundjiun  43540  meaiunincf  43563  pimgtmnf2  43790  smfpimcc  43880  smfsup  43886  smfinflem  43889  smfinf  43890  cbvral2  44127