Theorem cbvralvw 3243

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3372 with a disjoint variable condition, which does not require ax-10 2141, ax-11 2158, ax-12 2178, ax-13 2380. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2380. (Revised by GG, 10-Jan-2024.)

Hypothesis

Ref	Expression
cbvralvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralvw	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralvw

Step	Hyp	Ref	Expression
1		eleq1w 2827	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2035	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3068	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ral 3068

This theorem is referenced by:  cbvraldva  3245  cbvral2vw  3247  cbvral3vw  3249  cbvral4vw  3250  reu7  3754  cbviinv  5064  disjxun  5164  reusv3i  5422  wereu2  5697  cnvpo  6318  frpomin  6372  f1mpt  7298  dfwe2  7809  tfinds  7897  frrlem1  8327  wfrlem1OLD  8364  tfrlem1  8432  tfrlem12  8445  rdglem1  8471  tz7.48lem  8497  cbvixpv  8973  nneneq  9272  nneneqOLD  9284  marypha1lem  9502  supub  9528  suplub  9529  ordtypecbv  9586  ordtypelem3  9589  ordtypelem9  9595  wemaplem1  9615  brwdom3  9651  ttrclss  9789  ttrclselem2  9795  tcrank  9953  infxpenc2  10091  aceq1  10186  aceq2  10188  dfac5  10198  dfac9  10206  dfac12lem3  10215  kmlem12  10231  kmlem14  10233  cofsmo  10338  infpssrlem4  10375  isfin3ds  10398  isf32lem2  10423  isf32lem11  10432  isf33lem  10435  domtriomlem  10511  axdc3  10523  zorn2lem7  10571  zorn2g  10572  fpwwe2cbv  10699  fpwwecbv  10713  pwfseq  10733  axgroth6  10897  dedekind  11453  suprleub  12261  infregelb  12279  nnsub  12337  uzwo  12976  ublbneg  12998  zsupss  13002  xrub  13374  fsuppmapnn0fiubex  14043  monoord2  14084  faclbnd4lem4  14345  bccl  14371  hashbc  14502  wrdind  14770  wrd2ind  14771  reuccatpfxs1  14795  cau3lem  15403  climmpt2  15619  caucvgrlem  15721  caurcvg2  15726  caucvgb  15728  fsum0diag2  15831  incexclem  15884  cvgrat  15931  mertenslem2  15933  mertens  15934  sqrt2irr  16297  gcdcllem1  16545  lcmfunsnlem1  16684  lcmfunsnlem2lem1  16685  prmind2  16732  prmpwdvds  16951  prmreclem5  16967  prmreclem6  16968  vdwlem7  17034  vdwlem10  17037  vdwlem13  17040  vdwnn  17045  ramcl  17076  isacs2  17711  catpropd  17767  grpinvalem  18711  grpinva  18712  gsumvalx  18714  mndind  18863  issubg4  19185  isnsg2  19196  elnmz  19203  gsmsymgreqlem2  19473  psgnunilem5  19536  psgnunilem3  19538  efgsdm  19772  gsummptnn0fzfv  20029  pgpfac1lem5  20123  pgpfac1  20124  pgpfac  20128  ablfaclem3  20131  lbsextg  21187  evlslem2  22126  mpfind  22154  cply1mul  22321  mdetuni0  22648  m2cpminvid2lem  22781  mp2pm2mplem4  22836  chcoeffeqlem  22912  cayhamlem3  22914  elcls3  23112  isclo2  23117  neiptopnei  23161  tgcn  23281  subbascn  23283  txcmplem2  23671  kqfvima  23759  kqt0lem  23765  isr0  23766  r0cld  23767  regr1lem2  23769  fbun  23869  flftg  24025  fclsbas  24050  alexsubALTlem2  24077  alexsubALTlem4  24079  ptcmplem4  24084  tsmsxplem1  24182  tsmsxp  24184  ustuqtop  24276  utopsnneip  24278  prdsxmslem2  24563  isclmp  25149  iscau4  25332  caucfil  25336  iscmet3  25346  bcthlem5  25381  bcth  25382  ovolicc2lem5  25575  uniioombllem6  25642  vitali  25667  ismbf3d  25708  itg1climres  25769  itg2seq  25797  itg2monolem1  25805  itg2mono  25808  rolle  26048  dvlipcn  26053  dvivthlem1  26067  ply1divex  26196  fta1g  26229  dgrco  26335  plydivex  26357  fta1  26368  vieta1  26372  ulmcaulem  26455  ulmcau  26456  abelthlem8  26501  wilth  27132  fta  27141  fsumdvdsmul  27256  dchrelbas3  27300  2sqlem6  27485  2sqlem10  27490  dchrisumlem3  27553  dchrisum  27554  dchrmusumlema  27555  dchrvmasumlema  27562  dchrisum0lema  27576  pntibndlem3  27654  pntlem3  27671  pntleml  27673  pnt3  27674  ostth2lem2  27696  ostth  27701  nosupcbv  27765  nosupdm  27767  nosupbnd1lem4  27774  nosupbnd2  27779  noinfcbv  27780  noinfdm  27782  noinfres  27785  noinfbnd1lem1  27786  noinfbnd2  27794  madebdayim  27944  madebday  27956  cofss  27982  coiniss  27983  precsexlem9  28257  n0subs  28378  zs12bday  28442  axcontlem1  28997  axcontlem6  29002  uspgr2wlkeq  29682  crctcshwlkn0  29854  frgrwopreglem5ALT  30354  grpoideu  30541  ubthlem3  30904  adjsym  31865  lnopunilem1  32042  elunop2  32045  lnophm  32051  cnlnadjlem5  32103  mdbr3  32329  mdbr4  32330  dmdbr3  32337  dmdbr4  32338  mddmd2  32341  fprodex01  32829  wrdt2ind  32920  toslublem  32945  tosglblem  32947  chnind  32983  chnub  32984  archiabl  33178  isarchiofld  33312  1arithidom  33530  1arithufdlem3  33539  fedgmul  33644  constrconj  33735  qtophaus  33782  lmdvg  33899  prodindf  33987  esumcvg  34050  unelldsys  34122  ldgenpisyslem1  34127  eulerpartlemsv3  34326  eulerpartlemgvv  34341  signstfvneq0  34549  reprinfz1  34599  tgoldbachgtd  34639  bnj1185  34769  bnj222  34859  bnj517  34861  bnj1452  35028  bnj1463  35031  derangenlem  35139  subfacp1lem6  35153  subfacp1  35154  resconn  35214  cvmscbv  35226  sat1el2xp  35347  untangtr  35676  dfon2lem3  35749  dfon2lem7  35753  nn0prpwlem  36288  neibastop3  36328  fnemeet2  36333  weiunlem2  36429  fvineqsnf1  37376  fvineqsneu  37377  pibt2  37383  phpreu  37564  poimirlem27  37607  heicant  37615  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  mbfresfi  37626  upixp  37689  sdclem2  37702  fdc  37705  mettrifi  37717  heiborlem5  37775  heiborlem10  37780  heibor  37781  bfp  37784  disjressuc2  38344  cdleme25cv  40315  cdleme40v  40426  aks4d1p7  42040  aks6d1c1p3  42067  aks6d1c1p4  42068  supinf  42237  fsuppind  42545  mzpclval  42681  dford3lem1  42983  fnwe2lem1  43007  aomclem3  43013  aomclem4  43014  aomclem8  43018  dfac11  43019  hbtlem5  43085  nadd1suc  43354  ntrk2imkb  43999  ntrclsk2  44030  ntrclsk4  44034  fnchoice  44929  cncmpmax  44932  wessf1ornlem  45092  disjinfi  45099  rnmptbdd  45154  rnmptbd2  45158  rnmptbd  45165  supxrunb3  45314  unb2ltle  45330  monoord2xrv  45399  uzubioo2  45487  mccl  45519  climsuse  45529  limsupre  45562  limsuppnf  45632  limsupubuz  45634  limsupmnf  45642  limsupre2  45646  limsupmnfuz  45648  limsupre2mpt  45651  limsupre3  45654  limsupre3mpt  45655  limsupre3uzlem  45656  limsupre3uz  45657  limsupreuz  45658  limsupvaluz2  45659  limsupreuzmpt  45660  climuz  45665  lmbr3  45668  limsupge  45682  liminflelimsup  45697  liminfreuz  45724  xlimpnfxnegmnf  45735  cnrefiisp  45751  xlimmnf  45762  xlimpnf  45763  xlimmnfmpt  45764  xlimpnfmpt  45765  dfxlim2  45769  dvbdfbdioolem2  45850  dvbdfbdioo  45851  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem3  45869  stoweidlem7  45928  stoweidlem15  45936  stoweidlem35  45956  wallispilem3  45988  fourierdlem68  46095  fourierdlem71  46098  fourierdlem73  46100  fourierdlem87  46114  fourierdlem100  46127  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem109  46136  fourierdlem112  46139  etransc  46204  qndenserrnbllem  46215  dfsalgen2  46262  subsaliuncl  46279  meaiuninclem  46401  ovnsubaddlem2  46492  hoidmvlelem5  46520  hoidmvle  46521  hoiqssbllem3  46545  vonioo  46603  vonicc  46606  issmf  46649  issmfle  46666  issmfgt  46677  issmfge  46691  smfsuplem2  46733  2reuimp0  47029  uniimafveqt  47255  sbgoldbm  47658  mogoldbb  47659  bgoldbtbndlem4  47682  bgoldbtbnd  47683  nn0sumshdiglem1  48355  ipolub  48660  ipoglb  48663