Theorem raleqbi1dv 3317

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

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

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ral 3052  df-rex 3061

This theorem is referenced by:  raleqOLD  3319  isoeq4  7312  frrlem1  8283  frrlem13  8295  wfrlem1OLD  8320  wfrlem4OLD  8324  wfrlem15OLD  8335  smo11  8376  dffi2  9433  inficl  9435  dffi3  9441  dfom3  9659  aceq1  10129  dfac5lem4  10138  dfac5lem4OLD  10140  kmlem1  10163  kmlem10  10172  kmlem13  10175  kmlem14  10176  cofsmo  10281  infpssrlem4  10318  axdc3lem2  10463  elwina  10698  elina  10699  iswun  10716  eltskg  10762  elgrug  10804  elnp  10999  elnpi  11000  dfnn2  12251  dfnn3  12252  dfuzi  12682  coprmprod  16678  coprmproddvds  16680  ismri  17641  isprs  18306  isdrs  18311  ispos  18324  pospropd  18335  istos  18426  isdlat  18530  isipodrs  18545  mgmhmpropd  18674  issubmgm  18678  mhmpropd  18768  issubm  18779  subgacs  19142  nsgacs  19143  isghm  19196  isghmOLD  19197  ghmeql  19220  iscmn  19768  rnghmval  20398  dfrhm2  20432  zrrnghm  20494  islss  20889  lssacs  20922  lmhmeql  21011  islbs  21032  lbsextlem1  21117  lbsextlem3  21119  lbsextlem4  21120  isobs  21678  mat0dimcrng  22406  istopg  22831  isbasisg  22883  basis2  22887  eltg2  22894  iscldtop  23031  neipeltop  23065  isreg  23268  regsep  23270  isnrm  23271  islly  23404  isnlly  23405  llyi  23410  nllyi  23411  islly2  23420  cldllycmp  23431  isfbas  23765  fbssfi  23773  isust  24140  elutop  24170  ustuqtop  24183  utopsnneip  24185  ispsmet  24241  ismet  24260  isxmet  24261  metrest  24461  cncfval  24830  fmcfil  25222  iscfil3  25223  caucfil  25233  iscmet3  25243  cfilres  25246  minveclem3  25379  wilthlem2  27029  wilthlem3  27030  wilth  27031  dfn0s2  28253  dfconngr1  30115  isconngr  30116  1conngr  30121  isplig  30403  isgrpo  30424  isablo  30473  disjabrex  32509  disjabrexf  32510  isomnd  33015  isorng  33267  isrnsiga  34090  isldsys  34133  isros  34145  issros  34152  bnj1286  34996  bnj1452  35029  kur14lem9  35182  cvmscbv  35226  cvmsi  35233  cvmsval  35234  neibastop1  36323  neibastop2lem  36324  neibastop2  36325  rdgssun  37342  isbnd  37750  ismndo2  37844  rngomndo  37905  isidl  37984  ispsubsp  39710  sn-isghm  42643  isnacs  42674  mzpclval  42695  elmzpcl  42696  relpeq4  44920  nelsubc3lem  48985  isthinc  49253