Theorem raleqbi1dv 3307

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 3305	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ral 3054  df-rex 3064

This theorem is referenced by:  isoeq4  7265  frrlem1  8227  frrlem13  8239  smo11  8295  dffi2  9327  inficl  9329  dffi3  9335  dfom3  9560  aceq1  10031  dfac5lem4  10040  dfac5lem4OLD  10042  kmlem1  10065  kmlem10  10074  kmlem13  10077  kmlem14  10078  cofsmo  10183  infpssrlem4  10220  axdc3lem2  10365  elwina  10601  elina  10602  iswun  10619  eltskg  10665  elgrug  10707  elnp  10902  elnpi  10903  dfnn2  12179  dfnn3  12180  dfuzi  12612  coprmprod  16622  coprmproddvds  16624  ismri  17589  isprs  18254  isdrs  18259  ispos  18272  pospropd  18283  istos  18374  isdlat  18480  isipodrs  18495  mgmhmpropd  18658  issubmgm  18662  mhmpropd  18752  issubm  18763  subgacs  19128  nsgacs  19129  isghm  19182  isghmOLD  19183  ghmeql  19206  iscmn  19756  isomnd  20090  rnghmval  20412  dfrhm2  20446  zrrnghm  20509  isorng  20834  islss  20925  lssacs  20958  lmhmeql  21046  islbs  21067  lbsextlem1  21152  lbsextlem3  21154  lbsextlem4  21155  isobs  21696  mat0dimcrng  22454  istopg  22879  isbasisg  22931  basis2  22935  eltg2  22942  iscldtop  23079  neipeltop  23113  isreg  23316  regsep  23318  isnrm  23319  islly  23452  isnlly  23453  llyi  23458  nllyi  23459  islly2  23468  cldllycmp  23479  isfbas  23813  fbssfi  23821  isust  24188  elutop  24217  ustuqtop  24230  utopsnneip  24232  ispsmet  24288  ismet  24307  isxmet  24308  metrest  24508  cncfval  24874  fmcfil  25258  iscfil3  25259  caucfil  25269  iscmet3  25279  cfilres  25282  minveclem3  25415  wilthlem2  27051  wilthlem3  27052  wilth  27053  dfn0s2  28343  dfconngr1  30277  isconngr  30278  1conngr  30283  isplig  30566  isgrpo  30587  isablo  30636  disjabrex  32672  disjabrexf  32673  isrnsiga  34306  isldsys  34349  isros  34361  issros  34368  bnj1286  35210  bnj1452  35243  kur14lem9  35451  cvmscbv  35495  cvmsi  35502  cvmsval  35503  neibastop1  36596  neibastop2lem  36597  neibastop2  36598  dfttc4lem1  36765  rdgssun  37749  isbnd  38156  ismndo2  38250  rngomndo  38311  isidl  38390  ispsubsp  40246  sn-isghm  43132  isnacs  43162  mzpclval  43183  elmzpcl  43184  relpeq4  45400  permac8prim  45467  nelsubc3lem  49568  isthinc  49917