Theorem raleqbi1dv 3331

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1561  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-ral 3078  df-rex 3088

This theorem is referenced by:  isoeq4  7305  frrlem1  8268  frrlem13  8280  smo11  8336  dffi2  9370  inficl  9372  dffi3  9378  dfom3  9603  aceq1  10074  dfac5lem4  10083  dfac5lem4OLD  10085  kmlem1  10108  kmlem10  10117  kmlem13  10120  kmlem14  10121  cofsmo  10227  infpssrlem4  10264  axdc3lem2  10409  elwina  10645  elina  10646  iswun  10663  eltskg  10709  elgrug  10751  elnp  10946  elnpi  10947  dfnn2  12224  dfnn3  12225  dfuzi  12665  coprmprod  16696  coprmproddvds  16698  ismri  17664  isprs  18329  isdrs  18334  ispos  18347  pospropd  18358  istos  18449  isdlat  18555  isipodrs  18570  mgmhmpropd  18733  issubmgm  18737  mhmpropd  18827  issubm  18838  subgacs  19203  nsgacs  19204  isghm  19257  ghmeql  19280  iscmn  19830  isomnd  20164  rnghmval  20490  dfrhm2  20524  zrrnghm  20587  isorng  20911  islss  21002  lssacs  21035  lmhmeql  21123  islbs  21144  lbsextlem1  21229  lbsextlem3  21231  lbsextlem4  21232  isobs  21773  mat0dimcrng  22531  istopg  22956  isbasisg  23008  basis2  23012  eltg2  23019  iscldtop  23156  neipeltop  23190  isreg  23393  regsep  23395  isnrm  23396  islly  23529  isnlly  23530  llyi  23535  nllyi  23536  islly2  23545  cldllycmp  23556  isfbas  23890  fbssfi  23898  isust  24265  elutop  24294  ustuqtop  24307  utopsnneip  24309  ispsmet  24365  ismet  24384  isxmet  24385  metrest  24585  cncfval  24951  fmcfil  25335  iscfil3  25336  caucfil  25346  iscmet3  25356  cfilres  25359  minveclem3  25492  wilthlem2  27134  wilthlem3  27135  wilth  27136  dfn0s2  28426  dfconngr1  30391  isconngr  30392  1conngr  30397  isplig  30680  isgrpo  30701  isablo  30750  disjabrex  32783  disjabrexf  32784  isrnsiga  34411  isldsys  34454  isros  34466  issros  34473  bnj1286  35315  bnj1452  35348  kur14lem9  35565  cvmscbv  35609  cvmsi  35616  cvmsval  35617  nmulprop  36541  neibastop1  36720  neibastop2lem  36721  neibastop2  36722  dfttc4lem1  36889  rdgssun  37873  isbnd  38280  ismndo2  38374  rngomndo  38435  isidl  38514  ispsubsp  40370  sn-isghm  43256  isnacs  43286  mzpclval  43307  elmzpcl  43308  relpeq4  45524  permac8prim  45591  nelsubc3lem  49692  isthinc  50041