Theorem raleqbi1dv 3313

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	raleqbidvv 3309	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3045

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ral 3046  df-rex 3055

This theorem is referenced by:  raleqOLD  3315  isoeq4  7298  frrlem1  8268  frrlem13  8280  smo11  8336  dffi2  9381  inficl  9383  dffi3  9389  dfom3  9607  aceq1  10077  dfac5lem4  10086  dfac5lem4OLD  10088  kmlem1  10111  kmlem10  10120  kmlem13  10123  kmlem14  10124  cofsmo  10229  infpssrlem4  10266  axdc3lem2  10411  elwina  10646  elina  10647  iswun  10664  eltskg  10710  elgrug  10752  elnp  10947  elnpi  10948  dfnn2  12206  dfnn3  12207  dfuzi  12632  coprmprod  16638  coprmproddvds  16640  ismri  17599  isprs  18264  isdrs  18269  ispos  18282  pospropd  18293  istos  18384  isdlat  18488  isipodrs  18503  mgmhmpropd  18632  issubmgm  18636  mhmpropd  18726  issubm  18737  subgacs  19100  nsgacs  19101  isghm  19154  isghmOLD  19155  ghmeql  19178  iscmn  19726  rnghmval  20356  dfrhm2  20390  zrrnghm  20452  islss  20847  lssacs  20880  lmhmeql  20969  islbs  20990  lbsextlem1  21075  lbsextlem3  21077  lbsextlem4  21078  isobs  21636  mat0dimcrng  22364  istopg  22789  isbasisg  22841  basis2  22845  eltg2  22852  iscldtop  22989  neipeltop  23023  isreg  23226  regsep  23228  isnrm  23229  islly  23362  isnlly  23363  llyi  23368  nllyi  23369  islly2  23378  cldllycmp  23389  isfbas  23723  fbssfi  23731  isust  24098  elutop  24128  ustuqtop  24141  utopsnneip  24143  ispsmet  24199  ismet  24218  isxmet  24219  metrest  24419  cncfval  24788  fmcfil  25179  iscfil3  25180  caucfil  25190  iscmet3  25200  cfilres  25203  minveclem3  25336  wilthlem2  26986  wilthlem3  26987  wilth  26988  dfn0s2  28231  dfconngr1  30124  isconngr  30125  1conngr  30130  isplig  30412  isgrpo  30433  isablo  30482  disjabrex  32518  disjabrexf  32519  isomnd  33022  isorng  33284  isrnsiga  34110  isldsys  34153  isros  34165  issros  34172  bnj1286  35016  bnj1452  35049  kur14lem9  35208  cvmscbv  35252  cvmsi  35259  cvmsval  35260  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  rdgssun  37373  isbnd  37781  ismndo2  37875  rngomndo  37936  isidl  38015  ispsubsp  39746  sn-isghm  42668  isnacs  42699  mzpclval  42720  elmzpcl  42721  relpeq4  44944  permac8prim  45011  nelsubc3lem  49063  isthinc  49412