Theorem cbvralw 3280

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-11 2158  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2803  df-nfc 2878  df-ral 3045

This theorem is referenced by:  cbvralsvwOLD  3292  cbvralsvwOLDOLD  3293  cbviin  5001  disjxun  5105  ralxpf  5810  eqfnfv2f  7007  ralrnmptw  7066  dff13f  7230  ofrfval2  7674  fmpox  8046  ovmptss  8072  cbvixp  8887  mptelixpg  8908  boxcutc  8914  xpf1o  9103  indexfi  9311  ixpiunwdom  9543  dfac8clem  9985  acni2  9999  ac6c4  10434  iundom2g  10493  uniimadomf  10498  rabssnn0fi  13951  rlim2  15462  ello1mpt  15487  o1compt  15553  fsum00  15764  iserodd  16806  pcmptdvds  16865  catpropd  17670  invfuc  17939  gsummptnn0fz  19916  gsummoncoe1  22195  gsumply1eq  22196  fiuncmp  23291  elptr2  23461  ptcld  23500  ptclsg  23502  ptcnplem  23508  cnmpt11  23550  cnmpt21  23558  ovoliunlem3  25405  ovoliun  25406  ovoliun2  25407  finiunmbl  25445  volfiniun  25448  iunmbl  25454  voliun  25455  mbfeqalem1  25542  mbfsup  25565  mbfinf  25566  mbflim  25569  itg2split  25650  itgeqa  25715  itgfsum  25728  itgabs  25736  itggt0  25745  limciun  25795  dvlipcn  25899  dvfsumlem4  25936  dvfsum2  25941  itgsubst  25956  coeeq2  26147  ulmss  26306  leibpi  26852  rlimcnp  26875  o1cxp  26885  lgamgulmlem6  26944  fsumdvdscom  27095  lgseisenlem2  27287  disjunsn  32523  bnj110  34848  bnj1529  35060  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  poimirlem23  37637  itgabsnc  37683  itggt0cn  37684  totbndbnd  37783  aks6d1c1p5  42100  aks6d1c1rh  42113  aks6d1c7  42172  unitscyglem3  42185  disjinfi  45186  fmptf  45233  caucvgbf  45485  climinff  45609  idlimc  45624  fnlimabslt  45677  limsupref  45683  limsupbnd1f  45684  climbddf  45685  climinf2  45705  limsupubuz  45711  climinfmpt  45713  limsupmnf  45719  limsupre2  45723  limsupmnfuz  45725  limsupre3  45731  limsupre3uz  45734  limsupreuz  45735  climuz  45742  lmbr3  45745  limsupgt  45776  liminfreuz  45801  liminflt  45803  xlimpnfxnegmnf  45812  xlimmnf  45839  xlimpnf  45840  dfxlim2  45846  cncfshift  45872  stoweidlem31  46029  iundjiun  46458  meaiunincf  46481  pimgtmnf2  46712  smfpimcc  46806  smfsup  46812  smfinflem  46815  smfinf  46816  cbvral2  47104