Theorem raleqbi1dv 3309

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

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

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 2709

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

This theorem is referenced by:  raleqOLD  3311  isoeq4  7268  frrlem1  8230  frrlem13  8242  smo11  8298  dffi2  9330  inficl  9332  dffi3  9338  dfom3  9560  aceq1  10031  dfac5lem4  10040  dfac5lem4OLD  10042  kmlem1  10065  kmlem10  10074  kmlem13  10077  kmlem14  10078  cofsmo  10183  infpssrlem4  10220  axdc3lem2  10365  elwina  10601  elina  10602  iswun  10619  eltskg  10665  elgrug  10707  elnp  10902  elnpi  10903  dfnn2  12162  dfnn3  12163  dfuzi  12587  coprmprod  16592  coprmproddvds  16594  ismri  17558  isprs  18223  isdrs  18228  ispos  18241  pospropd  18252  istos  18343  isdlat  18449  isipodrs  18464  mgmhmpropd  18627  issubmgm  18631  mhmpropd  18721  issubm  18732  subgacs  19094  nsgacs  19095  isghm  19148  isghmOLD  19149  ghmeql  19172  iscmn  19722  isomnd  20056  rnghmval  20380  dfrhm2  20414  zrrnghm  20473  isorng  20798  islss  20889  lssacs  20922  lmhmeql  21011  islbs  21032  lbsextlem1  21117  lbsextlem3  21119  lbsextlem4  21120  isobs  21679  mat0dimcrng  22418  istopg  22843  isbasisg  22895  basis2  22899  eltg2  22906  iscldtop  23043  neipeltop  23077  isreg  23280  regsep  23282  isnrm  23283  islly  23416  isnlly  23417  llyi  23422  nllyi  23423  islly2  23432  cldllycmp  23443  isfbas  23777  fbssfi  23785  isust  24152  elutop  24181  ustuqtop  24194  utopsnneip  24196  ispsmet  24252  ismet  24271  isxmet  24272  metrest  24472  cncfval  24841  fmcfil  25232  iscfil3  25233  caucfil  25243  iscmet3  25253  cfilres  25256  minveclem3  25389  wilthlem2  27039  wilthlem3  27040  wilth  27041  dfn0s2  28332  dfconngr1  30267  isconngr  30268  1conngr  30273  isplig  30555  isgrpo  30576  isablo  30625  disjabrex  32660  disjabrexf  32661  isrnsiga  34272  isldsys  34315  isros  34327  issros  34334  bnj1286  35177  bnj1452  35210  kur14lem9  35410  cvmscbv  35454  cvmsi  35461  cvmsval  35462  neibastop1  36555  neibastop2lem  36556  neibastop2  36557  rdgssun  37585  isbnd  37983  ismndo2  38077  rngomndo  38138  isidl  38217  ispsubsp  40073  sn-isghm  42983  isnacs  43013  mzpclval  43034  elmzpcl  43035  relpeq4  45255  permac8prim  45322  nelsubc3lem  49382  isthinc  49731