Theorem cbvralvw 3243

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3352 with a disjoint variable condition, which does not require ax-10 2179, ax-11 2196, ax-12 2215, ax-13 2404. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2404. (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 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2070	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3080	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3080	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   ∈ wcel 2146  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2838  df-ral 3080

This theorem is used by:  cbvraldva  3245  cbvral2vw  3247  cbvral3vw  3249  cbvral4vw  3250  reu7  3692  cbviinv  5000  disjxun  5103  reusv3i  5369  wereu2  5651  cnvpo  6296  frpomin  6349  f1mpt  7272  dfwe2  7795  tfinds  7878  fnwe2lem2  8156  frrlem1  8315  tfrlem1  8394  tfrlem12  8408  rdglem1  8434  tz7.48lemOLD  8462  cbvixpv  8954  nneneq  9232  marypha1lem  9435  supub  9461  suplub  9462  ordtypecbv  9521  ordtypelem3  9524  ordtypelem9  9530  wemaplem1  9550  brwdom3  9586  ttrclss  9731  ttrclselem2  9737  tcrank  9911  infxpenc2  10111  aceq1  10206  aceq2  10208  dfac5  10217  dfac9  10225  dfac12lem3  10234  kmlem12  10250  kmlem14  10252  cofsmo  10357  infpssrlem4  10394  isfin3ds  10417  isf32lem2  10442  isf32lem11  10451  isf33lem  10454  domtriomlem  10530  axdc3  10542  zorn2lem7  10590  zorn2g  10591  fpwwe2cbv  10725  fpwwecbv  10739  pwfseq  10759  axgroth6  10923  dedekind  11483  suprleub  12293  infregelb  12311  nnsub  12392  uzwo  13048  ublbneg  13070  zsupss  13074  xrub  13452  fsuppmapnn0fiubex  14145  monoord2  14186  faclbnd4lem4  14450  bccl  14476  hashbc  14608  wrdind  14882  wrd2ind  14883  reuccatpfxs1  14907  cau3lem  15534  climmpt2  15752  caucvgrlem  15852  caurcvg2  15857  caucvgb  15859  fsum0diag2  15961  incexclem  16017  cvgrat  16064  mertenslem2  16066  mertens  16067  sqrt2irr  16429  gcdcllem1  16681  lcmfunsnlem1  16824  lcmfunsnlem2lem1  16825  prmind2  16872  prmpwdvds  17094  prmreclem5  17110  prmreclem6  17111  vdwlem7  17177  vdwlem10  17180  vdwlem13  17183  vdwnn  17188  ramcl  17219  isacs2  17839  catpropd  17895  chnind  18807  chnub  18808  grpinvalem  18866  grpinva  18867  gsumvalx  18877  mndind  19036  issubg4  19368  isnsg2  19378  elnmz  19385  gsmsymgreqlem2  19657  psgnunilem5  19720  psgnunilem3  19722  efgsdm  19956  gsummptnn0fzfv  20213  pgpfac1lem5  20307  pgpfac1  20308  pgpfac  20312  ablfaclem3  20315  lbsextg  21452  evlslem2  22400  mpfind  22436  cply1mul  22626  mdetuni0  22948  m2cpminvid2lem  23084  mp2pm2mplem4  23139  chcoeffeqlem  23215  cayhamlem3  23217  elcls3  23413  isclo2  23418  neiptopnei  23462  tgcn  23582  subbascn  23584  txcmplem2  23973  kqfvima  24061  kqt0lem  24067  isr0  24068  r0cld  24069  regr1lem2  24071  fbun  24171  flftg  24327  fclsbas  24352  alexsubALTlem2  24379  alexsubALTlem4  24381  ptcmplem4  24386  tsmsxplem1  24484  tsmsxp  24486  ustuqtop  24577  utopsnneip  24579  prdsxmslem2  24860  isclmp  25430  iscau4  25612  caucfil  25616  iscmet3  25626  bcthlem5  25661  bcth  25662  ovolicc2lem5  25854  uniioombllem6  25921  vitali  25946  ismbf3d  25987  itg1climres  26047  itg2seq  26075  itg2monolem1  26083  itg2mono  26086  rolle  26322  dvlipcn  26326  dvivthlem1  26340  ply1divex  26467  fta1g  26500  dgrco  26606  plydivex  26630  fta1  26641  vieta1  26647  ulmcaulem  26733  ulmcau  26734  abelthlem8  26778  wilth  27410  fta  27419  fsumdvdsmul  27534  dchrelbas3  27577  2sqlem6  27762  2sqlem10  27767  dchrisumlem3  27830  dchrisum  27831  dchrmusumlema  27832  dchrvmasumlema  27839  dchrisum0lema  27853  pntibndlem3  27931  pntlem3  27948  pntleml  27950  pnt3  27951  ostth2lem2  27973  ostth  27978  nosupcbv  28071  nosupdm  28073  nosupbnd1lem4  28080  nosupbnd2  28085  noinfcbv  28086  noinfdm  28088  noinfres  28091  noinfbnd1lem1  28092  noinfbnd2  28100  madebdayim  28286  madebday  28298  cofss  28328  coiniss  28329  cutminmax  28334  precsexlem9  28613  onsfi  28754  n0subs  28761  bdayfinbndcbv  28864  bdayfinbndlem2  28866  z12zsodd  28880  axcontlem1  29554  axcontlem6  29559  uspgr2wlkeq  30238  crctcshwlkn0  30422  frgrwopreglem5ALT  30935  grpoideu  31123  ubthlem3  31486  adjsym  32447  lnopunilem1  32624  elunop2  32627  lnophm  32633  cnlnadjlem5  32685  mdbr3  32911  mdbr4  32912  dmdbr3  32919  dmdbr4  32920  mddmd2  32923  fprodex01  33469  prodindf  33482  wrdt2ind  33569  toslublem  33586  tosglblem  33588  archiabl  33812  isarchiofld  33813  elrgspnlem1  33856  elrgspnlem2  33857  elrgspnlem4  33859  elrgspnsubrunlem2  33862  1arithidom  34122  1arithufdlem3  34131  vietadeg1  34263  vieta  34265  fedgmul  34316  fldextrspunlsplem  34358  constrconj  34430  qtophaus  34521  lmdvg  34638  esumcvg  34771  unelldsys  34844  ldgenpisyslem1  34849  eulerpartlemsv3  35046  eulerpartlemgvv  35061  signstfvneq0  35254  reprinfz1  35304  tgoldbachgtd  35344  bnj1185  35476  bnj222  35566  bnj517  35568  bnj1452  35735  bnj1463  35738  werankwe  35800  derangenlem  36057  subfacp1lem6  36071  subfacp1  36072  resconn  36132  cvmscbv  36144  sat1el2xp  36265  mirimanoffr  36581  untangtr  36606  dfon2lem3  36674  dfon2lem7  36678  nadddilem2  37097  nadddilem4  37099  nn0prpwlem  37237  neibastop3  37277  fnemeet2  37282  weiunlem  37378  mh-infprim2bi  37462  mh-infprim3bi  37463  fvineqsnf1  38473  fvineqsneu  38474  pibt2  38480  phpreu  38667  poimirlem27  38705  heicant  38713  mblfinlem2  38716  ovoliunnfl  38720  voliunnfl  38722  mbfresfi  38724  upixp  38803  sdclem2  38816  fdc  38819  mettrifi  38831  heiborlem5  38889  heiborlem10  38894  heibor  38895  bfp  38898  disjressuc2  39483  cdleme25cv  41555  cdleme40v  41666  aks4d1p7  43273  aks6d1c1p3  43300  aks6d1c1p4  43301  supinf  43433  fsuppind  43758  mzpclval  43876  dford3lem1  44173  aomclem3  44198  aomclem4  44199  aomclem8  44203  dfac11  44204  hbtlem5  44270  nadd1suc  44534  ntrk2imkb  45177  ntrclsk2  45208  ntrclsk4  45212  fnchoice  46185  cncmpmax  46188  wessf1ornlem  46339  disjinfi  46346  rnmptbdd  46396  rnmptbd2  46400  rnmptbd  46407  supxrunb3  46549  unb2ltle  46564  monoord2xrv  46632  uzubioo2  46718  mccl  46749  climsuse  46759  limsupre  46790  limsuppnf  46860  limsupubuz  46862  limsupmnf  46870  limsupre2  46874  limsupmnfuz  46876  limsupre2mpt  46879  limsupre3  46882  limsupre3mpt  46883  limsupre3uzlem  46884  limsupre3uz  46885  limsupreuz  46886  limsupvaluz2  46887  limsupreuzmpt  46888  climuz  46893  lmbr3  46896  limsupge  46910  liminflelimsup  46925  liminfreuz  46952  xlimpnfxnegmnf  46963  cnrefiisp  46979  xlimmnf  46990  xlimpnf  46991  xlimmnfmpt  46992  xlimpnfmpt  46993  dfxlim2  46997  dvbdfbdioolem2  47078  dvbdfbdioo  47079  ioodvbdlimc1lem1  47080  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnprodlem3  47097  stoweidlem7  47156  stoweidlem15  47164  stoweidlem35  47184  wallispilem3  47216  fourierdlem68  47323  fourierdlem71  47326  fourierdlem73  47328  fourierdlem87  47342  fourierdlem100  47355  fourierdlem103  47358  fourierdlem104  47359  fourierdlem107  47362  fourierdlem109  47364  fourierdlem112  47367  etransc  47432  qndenserrnbllem  47443  dfsalgen2  47490  subsaliuncl  47507  meaiuninclem  47629  ovnsubaddlem2  47720  hoidmvlelem5  47748  hoidmvle  47749  hoiqssbllem3  47773  vonioo  47831  vonicc  47834  issmf  47877  issmfle  47894  issmfgt  47905  issmfge  47919  smfsuplem2  47961  chnerlem1  48031  tmachlem-agreesn  48096  2reuimp0  48324  uniimafveqt  48602  sbgoldbm  49021  mogoldbb  49022  bgoldbtbndlem4  49045  bgoldbtbnd  49046  nn0sumshdiglem1  49872  ipolub  50241  ipoglb  50244