Theorem cbvralw 3279

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

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1785  ∀wral 3051

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-11 2163  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-clel 2811  df-nfc 2885  df-ral 3052

This theorem is referenced by:  cbvralsvwOLD  3290  cbviin  4978  disjxun  5083  ralxpf  5801  eqfnfv2f  6987  ralrnmptw  7046  dff13f  7210  ofrfval2  7652  fmpox  8020  ovmptss  8043  cbvixp  8862  mptelixpg  8883  boxcutc  8889  xpf1o  9077  indexfi  9270  ixpiunwdom  9505  dfac8clem  9954  acni2  9968  ac6c4  10403  iundom2g  10462  uniimadomf  10467  rabssnn0fi  13948  rlim2  15458  ello1mpt  15483  o1compt  15549  fsum00  15761  iserodd  16806  pcmptdvds  16865  catpropd  17675  invfuc  17944  gsummptnn0fz  19961  gsummoncoe1  22273  gsumply1eq  22274  fiuncmp  23369  elptr2  23539  ptcld  23578  ptclsg  23580  ptcnplem  23586  cnmpt11  23628  cnmpt21  23636  ovoliunlem3  25471  ovoliun  25472  ovoliun2  25473  finiunmbl  25511  volfiniun  25514  iunmbl  25520  voliun  25521  mbfeqalem1  25608  mbfsup  25631  mbfinf  25632  mbflim  25635  itg2split  25716  itgeqa  25781  itgfsum  25794  itgabs  25802  itggt0  25811  limciun  25861  dvlipcn  25961  dvfsumlem4  25996  dvfsum2  26001  itgsubst  26016  coeeq2  26207  ulmss  26362  leibpi  26906  rlimcnp  26929  o1cxp  26938  lgamgulmlem6  26997  fsumdvdscom  27148  lgseisenlem2  27339  disjunsn  32664  bnj110  35000  bnj1529  35212  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  poimirlem23  37964  itgabsnc  38010  itggt0cn  38011  totbndbnd  38110  aks6d1c1p5  42551  aks6d1c1rh  42564  aks6d1c7  42623  unitscyglem3  42636  disjinfi  45622  fmptf  45668  caucvgbf  45917  climinff  46041  idlimc  46056  fnlimabslt  46107  limsupref  46113  limsupbnd1f  46114  climbddf  46115  climinf2  46135  limsupubuz  46141  climinfmpt  46143  limsupmnf  46149  limsupre2  46153  limsupmnfuz  46155  limsupre3  46161  limsupre3uz  46164  limsupreuz  46165  climuz  46172  lmbr3  46175  limsupgt  46206  liminfreuz  46231  liminflt  46233  xlimpnfxnegmnf  46242  xlimmnf  46269  xlimpnf  46270  dfxlim2  46276  cncfshift  46302  stoweidlem31  46459  iundjiun  46888  meaiunincf  46911  pimgtmnf2  47142  smfpimcc  47236  smfsup  47242  smfinflem  47245  smfinf  47246  cbvral2  47551