Theorem cbvralw 3282

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

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

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 2804  df-nfc 2879  df-ral 3046

This theorem is referenced by:  cbvralsvwOLD  3294  cbvralsvwOLDOLD  3295  cbviin  5004  disjxun  5108  ralxpf  5813  eqfnfv2f  7010  ralrnmptw  7069  dff13f  7233  ofrfval2  7677  fmpox  8049  ovmptss  8075  cbvixp  8890  mptelixpg  8911  boxcutc  8917  xpf1o  9109  indexfi  9318  ixpiunwdom  9550  dfac8clem  9992  acni2  10006  ac6c4  10441  iundom2g  10500  uniimadomf  10505  rabssnn0fi  13958  rlim2  15469  ello1mpt  15494  o1compt  15560  fsum00  15771  iserodd  16813  pcmptdvds  16872  catpropd  17677  invfuc  17946  gsummptnn0fz  19923  gsummoncoe1  22202  gsumply1eq  22203  fiuncmp  23298  elptr2  23468  ptcld  23507  ptclsg  23509  ptcnplem  23515  cnmpt11  23557  cnmpt21  23565  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  finiunmbl  25452  volfiniun  25455  iunmbl  25461  voliun  25462  mbfeqalem1  25549  mbfsup  25572  mbfinf  25573  mbflim  25576  itg2split  25657  itgeqa  25722  itgfsum  25735  itgabs  25743  itggt0  25752  limciun  25802  dvlipcn  25906  dvfsumlem4  25943  dvfsum2  25948  itgsubst  25963  coeeq2  26154  ulmss  26313  leibpi  26859  rlimcnp  26882  o1cxp  26892  lgamgulmlem6  26951  fsumdvdscom  27102  lgseisenlem2  27294  disjunsn  32530  bnj110  34855  bnj1529  35067  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  poimirlem23  37644  itgabsnc  37690  itggt0cn  37691  totbndbnd  37790  aks6d1c1p5  42107  aks6d1c1rh  42120  aks6d1c7  42179  unitscyglem3  42192  disjinfi  45193  fmptf  45240  caucvgbf  45492  climinff  45616  idlimc  45631  fnlimabslt  45684  limsupref  45690  limsupbnd1f  45691  climbddf  45692  climinf2  45712  limsupubuz  45718  climinfmpt  45720  limsupmnf  45726  limsupre2  45730  limsupmnfuz  45732  limsupre3  45738  limsupre3uz  45741  limsupreuz  45742  climuz  45749  lmbr3  45752  limsupgt  45783  liminfreuz  45808  liminflt  45810  xlimpnfxnegmnf  45819  xlimmnf  45846  xlimpnf  45847  dfxlim2  45853  cncfshift  45879  stoweidlem31  46036  iundjiun  46465  meaiunincf  46488  pimgtmnf2  46719  smfpimcc  46813  smfsup  46819  smfinflem  46822  smfinf  46823  cbvral2  47108