Theorem raleqbi1dv 3339

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ral 3086  df-rex 3096

This theorem is referenced by:  isoeq4  7319  frrlem1  8282  frrlem13  8294  smo11  8350  dffi2  9382  inficl  9384  dffi3  9390  dfom3  9615  aceq1  10100  dfac5lem4  10109  kmlem1  10133  kmlem10  10142  kmlem13  10145  kmlem14  10146  cofsmo  10252  infpssrlem4  10289  axdc3lem2  10434  elwina  10670  elina  10671  iswun  10688  eltskg  10734  elgrug  10776  elnp  10971  elnpi  10972  dfnn2  12245  dfnn3  12246  dfuzi  12686  coprmprod  16718  coprmproddvds  16720  ismri  17686  isprs  18351  isdrs  18356  ispos  18369  pospropd  18380  istos  18471  isdlat  18577  isipodrs  18592  mgmhmpropd  18755  issubmgm  18759  mhmpropd  18849  issubm  18860  subgacs  19226  nsgacs  19227  isghm  19285  ghmeql  19308  iscmn  19858  isomnd  20192  rnghmval  20521  dfrhm2  20555  zrrnghm  20620  isorng  20941  islss  21032  lssacs  21065  lmhmeql  21153  islbs  21174  lbsextlem1  21259  lbsextlem3  21261  lbsextlem4  21262  isobs  21838  mat0dimcrng  22595  istopg  23020  isbasisg  23072  basis2  23076  eltg2  23083  iscldtop  23220  neipeltop  23254  isreg  23457  regsep  23459  isnrm  23460  islly  23593  isnlly  23594  llyi  23599  nllyi  23600  islly2  23609  cldllycmp  23620  isfbas  23954  fbssfi  23962  isust  24329  elutop  24358  ustuqtop  24371  utopsnneip  24373  ispsmet  24429  ismet  24448  isxmet  24449  metrest  24649  cncfval  25015  fmcfil  25399  iscfil3  25400  caucfil  25410  iscmet3  25420  cfilres  25423  minveclem3  25556  wilthlem2  27198  wilthlem3  27199  wilth  27200  dfn0s2  28490  dfconngr1  30479  isconngr  30480  1conngr  30485  isplig  30768  isgrpo  30789  isablo  30838  disjabrex  32867  disjabrexf  32868  isrnsiga  34447  isldsys  34490  isros  34502  issros  34509  bnj1286  35351  bnj1452  35384  kur14lem9  35604  cvmscbv  35648  cvmsi  35655  cvmsval  35656  nmulprop  36580  neibastop1  36758  neibastop2lem  36759  neibastop2  36760  dfttc4lem1  36927  rdgssun  37911  isbnd  38318  ismndo2  38412  rngomndo  38473  isidl  38552  ispsubsp  40408  sn-isghm  43296  isnacs  43326  mzpclval  43347  elmzpcl  43348  relpeq4  45547  permac8prim  45614  nelsubc3lem  49732  isthinc  50081