Theorem raleqbi1dv 3338

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ral 3062  df-rex 3071

This theorem is referenced by:  raleqOLD  3340  isoeq4  7340  frrlem1  8311  frrlem13  8323  wfrlem1OLD  8348  wfrlem4OLD  8352  wfrlem15OLD  8363  smo11  8404  dffi2  9463  inficl  9465  dffi3  9471  dfom3  9687  aceq1  10157  dfac5lem4  10166  dfac5lem4OLD  10168  kmlem1  10191  kmlem10  10200  kmlem13  10203  kmlem14  10204  cofsmo  10309  infpssrlem4  10346  axdc3lem2  10491  elwina  10726  elina  10727  iswun  10744  eltskg  10790  elgrug  10832  elnp  11027  elnpi  11028  dfnn2  12279  dfnn3  12280  dfuzi  12709  coprmprod  16698  coprmproddvds  16700  ismri  17674  isprs  18342  isdrs  18347  ispos  18360  pospropd  18372  istos  18463  isdlat  18567  isipodrs  18582  mgmhmpropd  18711  issubmgm  18715  mhmpropd  18805  issubm  18816  subgacs  19179  nsgacs  19180  isghm  19233  isghmOLD  19234  ghmeql  19257  iscmn  19807  rnghmval  20440  dfrhm2  20474  zrrnghm  20536  islss  20932  lssacs  20965  lmhmeql  21054  islbs  21075  lbsextlem1  21160  lbsextlem3  21162  lbsextlem4  21163  isobs  21740  mat0dimcrng  22476  istopg  22901  isbasisg  22954  basis2  22958  eltg2  22965  iscldtop  23103  neipeltop  23137  isreg  23340  regsep  23342  isnrm  23343  islly  23476  isnlly  23477  llyi  23482  nllyi  23483  islly2  23492  cldllycmp  23503  isfbas  23837  fbssfi  23845  isust  24212  elutop  24242  ustuqtop  24255  utopsnneip  24257  ispsmet  24314  ismet  24333  isxmet  24334  metrest  24537  cncfval  24914  fmcfil  25306  iscfil3  25307  caucfil  25317  iscmet3  25327  cfilres  25330  minveclem3  25463  wilthlem2  27112  wilthlem3  27113  wilth  27114  dfn0s2  28336  dfconngr1  30207  isconngr  30208  1conngr  30213  isplig  30495  isgrpo  30516  isablo  30565  disjabrex  32595  disjabrexf  32596  isomnd  33078  isorng  33329  isrnsiga  34114  isldsys  34157  isros  34169  issros  34176  bnj1286  35033  bnj1452  35066  kur14lem9  35219  cvmscbv  35263  cvmsi  35270  cvmsval  35271  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  rdgssun  37379  isbnd  37787  ismndo2  37881  rngomndo  37942  isidl  38021  ispsubsp  39747  sn-isghm  42683  isnacs  42715  mzpclval  42736  elmzpcl  42737  relpeq4  44968  isthinc  49069