Theorem raleqbi1dv 3305

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ral 3052  df-rex 3062

This theorem is referenced by:  isoeq4  7275  frrlem1  8236  frrlem13  8248  smo11  8304  dffi2  9336  inficl  9338  dffi3  9344  dfom3  9568  aceq1  10039  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem1  10073  kmlem10  10082  kmlem13  10085  kmlem14  10086  cofsmo  10191  infpssrlem4  10228  axdc3lem2  10373  elwina  10609  elina  10610  iswun  10627  eltskg  10673  elgrug  10715  elnp  10910  elnpi  10911  dfnn2  12187  dfnn3  12188  dfuzi  12620  coprmprod  16630  coprmproddvds  16632  ismri  17597  isprs  18262  isdrs  18267  ispos  18280  pospropd  18291  istos  18382  isdlat  18488  isipodrs  18503  mgmhmpropd  18666  issubmgm  18670  mhmpropd  18760  issubm  18771  subgacs  19136  nsgacs  19137  isghm  19190  isghmOLD  19191  ghmeql  19214  iscmn  19764  isomnd  20098  rnghmval  20420  dfrhm2  20454  zrrnghm  20513  isorng  20838  islss  20929  lssacs  20962  lmhmeql  21050  islbs  21071  lbsextlem1  21156  lbsextlem3  21158  lbsextlem4  21159  isobs  21700  mat0dimcrng  22435  istopg  22860  isbasisg  22912  basis2  22916  eltg2  22923  iscldtop  23060  neipeltop  23094  isreg  23297  regsep  23299  isnrm  23300  islly  23433  isnlly  23434  llyi  23439  nllyi  23440  islly2  23449  cldllycmp  23460  isfbas  23794  fbssfi  23802  isust  24169  elutop  24198  ustuqtop  24211  utopsnneip  24213  ispsmet  24269  ismet  24288  isxmet  24289  metrest  24489  cncfval  24855  fmcfil  25239  iscfil3  25240  caucfil  25250  iscmet3  25260  cfilres  25263  minveclem3  25396  wilthlem2  27032  wilthlem3  27033  wilth  27034  dfn0s2  28324  dfconngr1  30258  isconngr  30259  1conngr  30264  isplig  30547  isgrpo  30568  isablo  30617  disjabrex  32652  disjabrexf  32653  isrnsiga  34257  isldsys  34300  isros  34312  issros  34319  bnj1286  35161  bnj1452  35194  kur14lem9  35396  cvmscbv  35440  cvmsi  35447  cvmsval  35448  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  dfttc4lem1  36710  rdgssun  37694  isbnd  38101  ismndo2  38195  rngomndo  38256  isidl  38335  ispsubsp  40191  sn-isghm  43106  isnacs  43136  mzpclval  43157  elmzpcl  43158  relpeq4  45374  permac8prim  45441  nelsubc3lem  49545  isthinc  49894