Theorem cbvralv 3383

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. (Contributed by NM, 28-Jan-1997.)

Hypothesis

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

Assertion

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

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

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

Proof of Theorem cbvralv

Step	Hyp	Ref	Expression
1		nfv 1873	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1873	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvral 3379	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  ∀wral 3088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clel 2846  df-nfc 2918  df-ral 3093

This theorem is referenced by:  cbvral2v  3392  cbvral3v  3394  reu7  3635  disjxun  4927  reusv3i  5158  wereu2  5404  cnvpo  5976  f1mpt  6844  grprinvlem  7202  grprinvd  7203  dfwe2  7312  tfinds  7390  wfrlem1  7757  tfrlem1  7816  tfrlem12  7829  rdglem1  7855  tz7.48lem  7880  nneneq  8496  marypha1lem  8692  supub  8718  suplub  8719  ordtypecbv  8776  ordtypelem3  8779  ordtypelem9  8785  wemaplem1  8805  brwdom3  8841  tcrank  9107  infxpenc2  9242  aceq1  9337  aceq2  9339  dfac5  9348  dfac9  9356  dfac12lem3  9365  kmlem12  9381  kmlem14  9383  cofsmo  9489  infpssrlem4  9526  isfin3ds  9549  isf32lem2  9574  isf32lem11  9583  isf33lem  9586  domtriomlem  9662  axdc3  9674  zorn2lem7  9722  zorn2g  9723  fpwwe2cbv  9850  fpwwecbv  9864  pwfseq  9884  axgroth6  10048  dedekind  10603  suprleub  11408  infregelb  11426  nnsub  11484  uzwo  12125  ublbneg  12147  zsupss  12151  xrub  12521  fsuppmapnn0fiubex  13175  monoord2  13216  faclbnd4lem4  13471  bccl  13497  hashbc  13624  wrdind  13915  wrdindOLD  13916  wrd2ind  13917  wrd2indOLD  13918  reuccats1OLD  13921  reuccatpfxs1  13956  cau3lem  14575  climmpt2  14791  caucvgrlem  14890  caurcvg2  14895  caucvgb  14897  fsum0diag2  14998  incexclem  15051  cvgrat  15099  mertenslem2  15101  mertens  15102  sqrt2irr  15462  gcdcllem1  15708  lcmfunsnlem1  15837  lcmfunsnlem2lem1  15838  prmind2  15885  prmpwdvds  16096  prmreclem5  16112  prmreclem6  16113  vdwlem7  16179  vdwlem10  16182  vdwlem13  16185  vdwnn  16190  ramcl  16221  isacs2  16782  catpropd  16837  gsumvalx  17738  mndind  17834  issubg4  18082  isnsg2  18093  elnmz  18102  gsmsymgreqlem2  18320  psgnunilem5  18383  psgnunilem5OLD  18384  psgnunilem3  18386  efgsdm  18614  gsummptnn0fzfv  18857  pgpfac1lem5  18951  pgpfac1  18952  pgpfac  18956  ablfaclem3  18959  lbsextg  19656  evlslem2  20005  mpfind  20029  cply1mul  20165  mdetuni0  20934  m2cpminvid2lem  21066  mp2pm2mplem4  21121  chcoeffeqlem  21197  cayhamlem3  21199  elcls3  21395  isclo2  21400  neiptopnei  21444  tgcn  21564  subbascn  21566  txcmplem2  21954  kqfvima  22042  kqt0lem  22048  isr0  22049  r0cld  22050  regr1lem2  22052  fbun  22152  flftg  22308  fclsbas  22333  alexsubALTlem2  22360  alexsubALTlem4  22362  ptcmplem4  22367  tsmsxplem1  22464  tsmsxp  22466  ustuqtop  22558  utopsnneip  22560  prdsxmslem2  22842  isclmp  23404  iscau4  23585  caucfil  23589  iscmet3  23599  bcthlem5  23634  bcth  23635  ovolicc2lem5  23825  uniioombllem6  23892  vitali  23917  ismbf3d  23958  itg1climres  24018  itg2seq  24046  itg2monolem1  24054  itg2mono  24057  rolle  24290  dvlipcn  24294  dvivthlem1  24308  ply1divex  24433  fta1g  24464  dgrco  24568  plydivex  24589  fta1  24600  vieta1  24604  ulmcaulem  24685  ulmcau  24686  abelthlem8  24730  wilth  25350  fta  25359  dchrelbas3  25516  2sqlem6  25701  2sqlem10  25706  dchrisumlem3  25769  dchrisum  25770  dchrmusumlema  25771  dchrvmasumlema  25778  dchrisum0lema  25792  pntibndlem3  25870  pntlem3  25887  pntleml  25889  pnt3  25890  ostth2lem2  25912  ostth  25917  axcontlem1  26453  axcontlem6  26458  uspgr2wlkeq  27130  crctcshwlkn0  27307  frgrwopreglem5ALT  27856  grpoideu  28063  ubthlem3  28427  adjsym  29391  lnopunilem1  29568  elunop2  29571  lnophm  29577  cnlnadjlem5  29629  mdbr3  29855  mdbr4  29856  dmdbr3  29863  dmdbr4  29864  mddmd2  29867  fprodex01  30294  toslublem  30392  tosglblem  30394  archiabl  30499  isarchiofld  30575  fedgmul  30662  qtophaus  30750  lmdvg  30846  prodindf  30932  esumcvg  30995  unelldsys  31068  ldgenpisyslem1  31073  eulerpartlemsv3  31270  eulerpartlemgvv  31285  signstfvneq0  31495  reprinfz1  31547  tgoldbachgtd  31587  bnj1185  31719  bnj222  31808  bnj517  31810  bnj1452  31975  bnj1463  31978  derangenlem  32009  subfacp1lem6  32023  subfacp1  32024  resconn  32084  cvmscbv  32096  sat1el2xp  32195  untangtr  32466  dfon2lem3  32556  dfon2lem7  32560  frpomin  32605  frrlem1  32650  nosupdm  32731  nosupbnd1lem4  32738  nosupbnd2  32743  nn0prpwlem  33197  neibastop3  33237  fnemeet2  33242  fvineqsnf1  34138  fvineqsneu  34139  pibt2  34145  phpreu  34323  poimirlem27  34366  heicant  34374  mblfinlem2  34377  ovoliunnfl  34381  voliunnfl  34383  mbfresfi  34385  upixp  34452  sdclem2  34465  fdc  34468  mettrifi  34480  heiborlem5  34541  heiborlem10  34546  heibor  34547  bfp  34550  cdleme25cv  36945  cdleme40v  37056  mzpclval  38723  dford3lem1  39025  fnwe2lem1  39052  aomclem3  39058  aomclem4  39059  aomclem8  39063  dfac11  39064  hbtlem5  39130  ntrk2imkb  39756  ntrclsk2  39787  ntrclsk4  39791  fnchoice  40711  cncmpmax  40714  wessf1ornlem  40875  disjinfi  40884  rnmptbdd  40949  rnmptbd2  40955  rnmptbd  40962  supxrunb3  41108  unb2ltle  41126  monoord2xrv  41197  uzubioo2  41282  mccl  41316  climsuse  41326  limsupre  41359  limsuppnfd  41420  limsuppnf  41429  limsupubuz  41431  limsupmnf  41439  limsupre2  41443  limsupmnfuz  41445  limsupre2mpt  41448  limsupre3  41451  limsupre3mpt  41452  limsupre3uzlem  41453  limsupre3uz  41454  limsupreuz  41455  limsupvaluz2  41456  limsupreuzmpt  41457  climuz  41462  lmbr3  41465  limsupge  41479  liminfreuz  41521  xlimpnfxnegmnf  41532  cnrefiisp  41548  xlimmnf  41559  xlimpnf  41560  xlimmnfmpt  41561  xlimpnfmpt  41562  dfxlim2  41566  dvbdfbdioolem2  41650  dvbdfbdioo  41651  ioodvbdlimc1lem1  41652  ioodvbdlimc1lem2  41653  ioodvbdlimc2lem  41655  dvnprodlem3  41669  stoweidlem7  41729  stoweidlem15  41737  stoweidlem35  41757  wallispilem3  41789  fourierdlem68  41896  fourierdlem71  41899  fourierdlem73  41901  fourierdlem87  41915  fourierdlem100  41928  fourierdlem103  41931  fourierdlem104  41932  fourierdlem107  41935  fourierdlem109  41937  fourierdlem112  41940  etransc  42005  qndenserrnbllem  42016  dfsalgen2  42061  subsaliuncl  42078  meaiuninclem  42199  ovnsubaddlem2  42290  hoidmvlelem5  42318  hoidmvle  42319  hoiqssbllem3  42343  vonioo  42401  vonicc  42404  issmf  42442  issmfle  42459  issmfgt  42470  issmfge  42483  smfsuplem2  42523  2reuimp0  42725  sbgoldbm  43323  mogoldbb  43324  bgoldbtbndlem4  43347  bgoldbtbnd  43348  nn0sumshdiglem1  44055