Theorem raleqbi1dv 3346

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ral 3068  df-rex 3077

This theorem is referenced by:  raleqOLD  3348  isoeq4  7356  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem4OLD  8368  wfrlem15OLD  8379  smo11  8420  dffi2  9492  inficl  9494  dffi3  9500  dfom3  9716  aceq1  10186  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem1  10220  kmlem10  10229  kmlem13  10232  kmlem14  10233  cofsmo  10338  infpssrlem4  10375  axdc3lem2  10520  elwina  10755  elina  10756  iswun  10773  eltskg  10819  elgrug  10861  elnp  11056  elnpi  11057  dfnn2  12306  dfnn3  12307  dfuzi  12734  coprmprod  16708  coprmproddvds  16710  ismri  17689  isprs  18367  isdrs  18371  ispos  18384  pospropd  18397  istos  18488  isdlat  18592  isipodrs  18607  mgmhmpropd  18736  issubmgm  18740  mhmpropd  18827  issubm  18838  subgacs  19201  nsgacs  19202  isghm  19255  isghmOLD  19256  ghmeql  19279  iscmn  19831  rnghmval  20466  dfrhm2  20500  zrrnghm  20562  islss  20955  lssacs  20988  lmhmeql  21077  islbs  21098  lbsextlem1  21183  lbsextlem3  21185  lbsextlem4  21186  isobs  21763  mat0dimcrng  22497  istopg  22922  isbasisg  22975  basis2  22979  eltg2  22986  iscldtop  23124  neipeltop  23158  isreg  23361  regsep  23363  isnrm  23364  islly  23497  isnlly  23498  llyi  23503  nllyi  23504  islly2  23513  cldllycmp  23524  isfbas  23858  fbssfi  23866  isust  24233  elutop  24263  ustuqtop  24276  utopsnneip  24278  ispsmet  24335  ismet  24354  isxmet  24355  metrest  24558  cncfval  24933  fmcfil  25325  iscfil3  25326  caucfil  25336  iscmet3  25346  cfilres  25349  minveclem3  25482  wilthlem2  27130  wilthlem3  27131  wilth  27132  dfn0s2  28354  dfconngr1  30220  isconngr  30221  1conngr  30226  isplig  30508  isgrpo  30529  isablo  30578  disjabrex  32604  disjabrexf  32605  isomnd  33051  isorng  33294  isrnsiga  34077  isldsys  34120  isros  34132  issros  34139  bnj1286  34995  bnj1452  35028  kur14lem9  35182  cvmscbv  35226  cvmsi  35233  cvmsval  35234  neibastop1  36325  neibastop2lem  36326  neibastop2  36327  rdgssun  37344  isbnd  37740  ismndo2  37834  rngomndo  37895  isidl  37974  ispsubsp  39702  sn-isghm  42628  isnacs  42660  mzpclval  42681  elmzpcl  42682  isthinc  48688