Theorem cbvralw 3274

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3272 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2372. (Revised by GG, 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 2894	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2894	. 2 ⊢ Ⅎ𝑦𝐴
3		cbvralw.1	. 2 ⊢ Ⅎ𝑦𝜑
4		cbvralw.2	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvralw.3	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvralfw 3272	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1784  ∀wral 3047

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 1968  ax-7 2009  ax-8 2113  ax-11 2160  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-clel 2806  df-nfc 2881  df-ral 3048

This theorem is referenced by:  cbvralsvwOLD  3285  cbvralsvwOLDOLD  3286  cbviin  4984  disjxun  5087  ralxpf  5785  eqfnfv2f  6968  ralrnmptw  7027  dff13f  7189  ofrfval2  7631  fmpox  7999  ovmptss  8023  cbvixp  8838  mptelixpg  8859  boxcutc  8865  xpf1o  9052  indexfi  9244  ixpiunwdom  9476  dfac8clem  9923  acni2  9937  ac6c4  10372  iundom2g  10431  uniimadomf  10436  rabssnn0fi  13893  rlim2  15403  ello1mpt  15428  o1compt  15494  fsum00  15705  iserodd  16747  pcmptdvds  16806  catpropd  17615  invfuc  17884  gsummptnn0fz  19898  gsummoncoe1  22223  gsumply1eq  22224  fiuncmp  23319  elptr2  23489  ptcld  23528  ptclsg  23530  ptcnplem  23536  cnmpt11  23578  cnmpt21  23586  ovoliunlem3  25432  ovoliun  25433  ovoliun2  25434  finiunmbl  25472  volfiniun  25475  iunmbl  25481  voliun  25482  mbfeqalem1  25569  mbfsup  25592  mbfinf  25593  mbflim  25596  itg2split  25677  itgeqa  25742  itgfsum  25755  itgabs  25763  itggt0  25772  limciun  25822  dvlipcn  25926  dvfsumlem4  25963  dvfsum2  25968  itgsubst  25983  coeeq2  26174  ulmss  26333  leibpi  26879  rlimcnp  26902  o1cxp  26912  lgamgulmlem6  26971  fsumdvdscom  27122  lgseisenlem2  27314  disjunsn  32574  bnj110  34870  bnj1529  35082  weiunpo  36507  weiunso  36508  weiunfr  36509  weiunse  36510  poimirlem23  37691  itgabsnc  37737  itggt0cn  37738  totbndbnd  37837  aks6d1c1p5  42153  aks6d1c1rh  42166  aks6d1c7  42225  unitscyglem3  42238  disjinfi  45237  fmptf  45284  caucvgbf  45535  climinff  45659  idlimc  45674  fnlimabslt  45725  limsupref  45731  limsupbnd1f  45732  climbddf  45733  climinf2  45753  limsupubuz  45759  climinfmpt  45761  limsupmnf  45767  limsupre2  45771  limsupmnfuz  45773  limsupre3  45779  limsupre3uz  45782  limsupreuz  45783  climuz  45790  lmbr3  45793  limsupgt  45824  liminfreuz  45849  liminflt  45851  xlimpnfxnegmnf  45860  xlimmnf  45887  xlimpnf  45888  dfxlim2  45894  cncfshift  45920  stoweidlem31  46077  iundjiun  46506  meaiunincf  46529  pimgtmnf2  46760  smfpimcc  46854  smfsup  46860  smfinflem  46863  smfinf  46864  cbvral2  47142