Theorem cbvralw 3303

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1779  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-11 2154  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-nf 1780  df-clel 2813  df-nfc 2889  df-ral 3059

This theorem is referenced by:  cbvralsvwOLD  3316  cbvralsvwOLDOLD  3317  cbviin  5041  disjxun  5145  ralxpf  5859  eqfnfv2f  7054  ralrnmptw  7113  dff13f  7275  ofrfval2  7717  fmpox  8090  ovmptss  8116  cbvixp  8952  mptelixpg  8973  boxcutc  8979  xpf1o  9177  indexfi  9397  ixpiunwdom  9627  dfac8clem  10069  acni2  10083  ac6c4  10518  iundom2g  10577  uniimadomf  10582  rabssnn0fi  14023  rlim2  15528  ello1mpt  15553  o1compt  15619  fsum00  15830  iserodd  16868  pcmptdvds  16927  catpropd  17753  invfuc  18030  gsummptnn0fz  20018  gsummoncoe1  22327  gsumply1eq  22328  fiuncmp  23427  elptr2  23597  ptcld  23636  ptclsg  23638  ptcnplem  23644  cnmpt11  23686  cnmpt21  23694  ovoliunlem3  25552  ovoliun  25553  ovoliun2  25554  finiunmbl  25592  volfiniun  25595  iunmbl  25601  voliun  25602  mbfeqalem1  25689  mbfsup  25712  mbfinf  25713  mbflim  25716  itg2split  25798  itgeqa  25863  itgfsum  25876  itgabs  25884  itggt0  25893  limciun  25943  dvlipcn  26047  dvfsumlem4  26084  dvfsum2  26089  itgsubst  26104  coeeq2  26295  ulmss  26454  leibpi  26999  rlimcnp  27022  o1cxp  27032  lgamgulmlem6  27091  fsumdvdscom  27242  lgseisenlem2  27434  disjunsn  32613  bnj110  34850  bnj1529  35062  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  poimirlem23  37629  itgabsnc  37675  itggt0cn  37676  totbndbnd  37775  aks6d1c1p5  42093  aks6d1c1rh  42106  aks6d1c7  42165  unitscyglem3  42178  disjinfi  45134  fmptf  45182  caucvgbf  45439  climinff  45566  idlimc  45581  fnlimabslt  45634  limsupref  45640  limsupbnd1f  45641  climbddf  45642  climinf2  45662  limsupubuz  45668  climinfmpt  45670  limsupmnf  45676  limsupre2  45680  limsupmnfuz  45682  limsupre3  45688  limsupre3uz  45691  limsupreuz  45692  climuz  45699  lmbr3  45702  limsupgt  45733  liminfreuz  45758  liminflt  45760  xlimpnfxnegmnf  45769  xlimmnf  45796  xlimpnf  45797  dfxlim2  45803  cncfshift  45829  stoweidlem31  45986  iundjiun  46415  meaiunincf  46438  pimgtmnf2  46669  smfpimcc  46763  smfsup  46769  smfinflem  46772  smfinf  46773  cbvral2  47052