Theorem cbvralw 3306

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

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

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 2007  ax-8 2110  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2816  df-nfc 2892  df-ral 3062

This theorem is referenced by:  cbvralsvwOLD  3319  cbvralsvwOLDOLD  3320  cbviin  5037  disjxun  5141  ralxpf  5857  eqfnfv2f  7055  ralrnmptw  7114  dff13f  7276  ofrfval2  7718  fmpox  8092  ovmptss  8118  cbvixp  8954  mptelixpg  8975  boxcutc  8981  xpf1o  9179  indexfi  9400  ixpiunwdom  9630  dfac8clem  10072  acni2  10086  ac6c4  10521  iundom2g  10580  uniimadomf  10585  rabssnn0fi  14027  rlim2  15532  ello1mpt  15557  o1compt  15623  fsum00  15834  iserodd  16873  pcmptdvds  16932  catpropd  17752  invfuc  18022  gsummptnn0fz  20004  gsummoncoe1  22312  gsumply1eq  22313  fiuncmp  23412  elptr2  23582  ptcld  23621  ptclsg  23623  ptcnplem  23629  cnmpt11  23671  cnmpt21  23679  ovoliunlem3  25539  ovoliun  25540  ovoliun2  25541  finiunmbl  25579  volfiniun  25582  iunmbl  25588  voliun  25589  mbfeqalem1  25676  mbfsup  25699  mbfinf  25700  mbflim  25703  itg2split  25784  itgeqa  25849  itgfsum  25862  itgabs  25870  itggt0  25879  limciun  25929  dvlipcn  26033  dvfsumlem4  26070  dvfsum2  26075  itgsubst  26090  coeeq2  26281  ulmss  26440  leibpi  26985  rlimcnp  27008  o1cxp  27018  lgamgulmlem6  27077  fsumdvdscom  27228  lgseisenlem2  27420  disjunsn  32607  bnj110  34872  bnj1529  35084  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  poimirlem23  37650  itgabsnc  37696  itggt0cn  37697  totbndbnd  37796  aks6d1c1p5  42113  aks6d1c1rh  42126  aks6d1c7  42185  unitscyglem3  42198  disjinfi  45197  fmptf  45245  caucvgbf  45500  climinff  45626  idlimc  45641  fnlimabslt  45694  limsupref  45700  limsupbnd1f  45701  climbddf  45702  climinf2  45722  limsupubuz  45728  climinfmpt  45730  limsupmnf  45736  limsupre2  45740  limsupmnfuz  45742  limsupre3  45748  limsupre3uz  45751  limsupreuz  45752  climuz  45759  lmbr3  45762  limsupgt  45793  liminfreuz  45818  liminflt  45820  xlimpnfxnegmnf  45829  xlimmnf  45856  xlimpnf  45857  dfxlim2  45863  cncfshift  45889  stoweidlem31  46046  iundjiun  46475  meaiunincf  46498  pimgtmnf2  46729  smfpimcc  46823  smfsup  46829  smfinflem  46832  smfinf  46833  cbvral2  47115