Theorem raleqbi1dv 3330

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ral 3078  df-rex 3088

This theorem is used by:  isoeq4  7328  frrlem1  8304  frrlem13  8316  smo11  8372  dffi2  9415  inficl  9417  dffi3  9423  dfom3  9648  aceq1  10196  dfac5lem4  10205  kmlem1  10229  kmlem10  10238  kmlem13  10241  kmlem14  10242  cofsmo  10347  infpssrlem4  10384  axdc3lem2  10529  elwina  10771  elina  10772  iswun  10789  eltskg  10835  elgrug  10877  elnp  11072  elnpi  11073  dfnn2  12348  dfnn3  12349  dfuzi  12790  coprmprod  16836  coprmproddvds  16838  ismri  17805  isprs  18470  isdrs  18475  ispos  18488  pospropd  18499  istos  18590  isdlat  18696  isipodrs  18711  mgmhmpropd  18887  issubmgm  18891  mhmpropd  18987  issubm  18998  subgacs  19371  nsgacs  19372  isghm  19430  ghmeql  19453  iscmn  20003  isomnd  20337  rnghmval  20670  dfrhm2  20704  zrrnghm  20788  isorng  21118  islss  21209  lssacs  21242  lmhmeql  21330  islbs  21351  lbsextlem1  21436  lbsextlem3  21438  lbsextlem4  21439  isobs  22026  mat0dimcrng  22785  istopg  23213  isbasisg  23265  basis2  23269  eltg2  23276  iscldtop  23413  neipeltop  23447  isreg  23650  regsep  23652  isnrm  23653  islly  23787  isnlly  23788  llyi  23793  nllyi  23794  islly2  23803  cldllycmp  23814  isfbas  24148  fbssfi  24156  isust  24523  elutop  24552  ustuqtop  24565  utopsnneip  24567  ispsmet  24623  ismet  24642  isxmet  24643  metrest  24843  cncfval  25209  fmcfil  25593  iscfil3  25594  caucfil  25604  iscmet3  25614  cfilres  25617  minveclem3  25750  wilthlem2  27396  wilthlem3  27397  wilth  27398  dfn0s2  28718  dfconngr1  30789  isconngr  30790  1conngr  30795  isplig  31078  isgrpo  31099  isablo  31148  disjabrex  33176  disjabrexf  33177  isrnsiga  34745  isldsys  34789  isros  34801  issros  34808  bnj1286  35649  bnj1452  35682  kur14lem9  35979  cvmscbv  36023  cvmsi  36030  cvmsval  36031  nmulprop  36939  neibastop1  37147  neibastop2lem  37148  neibastop2  37149  dfttc4lem1  37316  mh-inf3f1  37329  rdgssun  38301  isbnd  38714  ismndo2  38808  rngomndo  38869  isidl  38948  ispsubsp  40802  sn-isghm  43684  isnacs  43714  mzpclval  43735  elmzpcl  43736  relpeq4  45936  permac8prim  46003  nelsubc3lem  50177  isthinc  50526