Theorem raleqbi1dv 3333

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.)

Hypothesis

Ref	Expression
raleqbi1dv.1	⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
raleqbi1dv	⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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

Proof of Theorem raleqbi1dv

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	raleqbidvv 3331	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ral 3080  df-rex 3090

This theorem is used by:  isoeq4  7318  frrlem1  8279  frrlem13  8291  smo11  8347  dffi2  9379  inficl  9381  dffi3  9387  dfom3  9612  aceq1  10106  dfac5lem4  10115  kmlem1  10139  kmlem10  10148  kmlem13  10151  kmlem14  10152  cofsmo  10257  infpssrlem4  10294  axdc3lem2  10439  elwina  10675  elina  10676  iswun  10693  eltskg  10739  elgrug  10781  elnp  10976  elnpi  10977  dfnn2  12250  dfnn3  12251  dfuzi  12691  coprmprod  16723  coprmproddvds  16725  ismri  17691  isprs  18356  isdrs  18361  ispos  18374  pospropd  18385  istos  18476  isdlat  18582  isipodrs  18597  mgmhmpropd  18760  issubmgm  18764  mhmpropd  18854  issubm  18865  subgacs  19231  nsgacs  19232  isghm  19290  ghmeql  19313  iscmn  19863  isomnd  20197  rnghmval  20527  dfrhm2  20561  zrrnghm  20644  isorng  20973  islss  21064  lssacs  21097  lmhmeql  21185  islbs  21206  lbsextlem1  21291  lbsextlem3  21293  lbsextlem4  21294  isobs  21879  mat0dimcrng  22636  istopg  23061  isbasisg  23113  basis2  23117  eltg2  23124  iscldtop  23261  neipeltop  23295  isreg  23498  regsep  23500  isnrm  23501  islly  23634  isnlly  23635  llyi  23640  nllyi  23641  islly2  23650  cldllycmp  23661  isfbas  23995  fbssfi  24003  isust  24370  elutop  24399  ustuqtop  24412  utopsnneip  24414  ispsmet  24470  ismet  24489  isxmet  24490  metrest  24690  cncfval  25056  fmcfil  25440  iscfil3  25441  caucfil  25451  iscmet3  25461  cfilres  25464  minveclem3  25597  wilthlem2  27242  wilthlem3  27243  wilth  27244  dfn0s2  28534  dfconngr1  30548  isconngr  30549  1conngr  30554  isplig  30837  isgrpo  30858  isablo  30907  disjabrex  32936  disjabrexf  32937  isrnsiga  34512  isldsys  34555  isros  34567  issros  34574  bnj1286  35416  bnj1452  35449  kur14lem9  35714  cvmscbv  35758  cvmsi  35765  cvmsval  35766  nmulprop  36690  neibastop1  36898  neibastop2lem  36899  neibastop2  36900  dfttc4lem1  37067  rdgssun  38052  isbnd  38459  ismndo2  38553  rngomndo  38614  isidl  38693  ispsubsp  40547  sn-isghm  43433  isnacs  43463  mzpclval  43484  elmzpcl  43485  relpeq4  45684  permac8prim  45751  nelsubc3lem  49876  isthinc  50225