Theorem raleqbi1dv 3405

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895  df-ral 3145

This theorem is referenced by:  raleq  3407  isoeq4  7075  wfrlem1  7956  wfrlem4  7960  wfrlem15  7971  smo11  8003  dffi2  8889  inficl  8891  dffi3  8897  dfom3  9112  aceq1  9545  dfac5lem4  9554  kmlem1  9578  kmlem10  9587  kmlem13  9590  kmlem14  9591  cofsmo  9693  infpssrlem4  9730  axdc3lem2  9875  elwina  10110  elina  10111  iswun  10128  eltskg  10174  elgrug  10216  elnp  10411  elnpi  10412  dfnn2  11653  dfnn3  11654  dfuzi  12076  coprmprod  16007  coprmproddvds  16009  ismri  16904  isprs  17542  isdrs  17546  ispos  17559  istos  17647  pospropd  17746  isipodrs  17773  isdlat  17805  mhmpropd  17964  issubm  17970  subgacs  18315  nsgacs  18316  isghm  18360  ghmeql  18383  iscmn  18916  dfrhm2  19471  islss  19708  lssacs  19741  lmhmeql  19829  islbs  19850  lbsextlem1  19932  lbsextlem3  19934  lbsextlem4  19935  isobs  20866  mat0dimcrng  21081  istopg  21505  isbasisg  21557  basis2  21561  eltg2  21568  iscldtop  21705  neipeltop  21739  isreg  21942  regsep  21944  isnrm  21945  islly  22078  isnlly  22079  llyi  22084  nllyi  22085  islly2  22094  cldllycmp  22105  isfbas  22439  fbssfi  22447  isust  22814  elutop  22844  ustuqtop  22857  utopsnneip  22859  ispsmet  22916  ismet  22935  isxmet  22936  metrest  23136  cncfval  23498  fmcfil  23877  iscfil3  23878  caucfil  23888  iscmet3  23898  cfilres  23901  minveclem3  24034  wilthlem2  25648  wilthlem3  25649  wilth  25650  dfconngr1  27969  isconngr  27970  1conngr  27975  isplig  28255  isgrpo  28276  isablo  28325  disjabrex  30334  disjabrexf  30335  isomnd  30704  isorng  30874  isrnsiga  31374  isldsys  31417  isros  31429  issros  31436  bnj1286  32293  bnj1452  32326  kur14lem9  32463  cvmscbv  32507  cvmsi  32514  cvmsval  32515  frrlem1  33125  frrlem13  33137  neibastop1  33709  neibastop2lem  33710  neibastop2  33711  rdgssun  34661  isbnd  35060  ismndo2  35154  rngomndo  35215  isidl  35294  ispsubsp  36883  isnacs  39308  mzpclval  39329  elmzpcl  39330  mgmhmpropd  44059  issubmgm  44063  rnghmval  44169  zrrnghm  44195