Theorem raleqbi1dv 3339

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ral 3086  df-rex 3096

This theorem is referenced by:  isoeq4  7319  frrlem1  8283  frrlem13  8295  smo11  8351  dffi2  9383  inficl  9385  dffi3  9391  dfom3  9616  aceq1  10101  dfac5lem4  10110  kmlem1  10134  kmlem10  10143  kmlem13  10146  kmlem14  10147  cofsmo  10253  infpssrlem4  10290  axdc3lem2  10435  elwina  10671  elina  10672  iswun  10689  eltskg  10735  elgrug  10777  elnp  10972  elnpi  10973  dfnn2  12246  dfnn3  12247  dfuzi  12687  coprmprod  16719  coprmproddvds  16721  ismri  17687  isprs  18352  isdrs  18357  ispos  18370  pospropd  18381  istos  18472  isdlat  18578  isipodrs  18593  mgmhmpropd  18756  issubmgm  18760  mhmpropd  18850  issubm  18861  subgacs  19227  nsgacs  19228  isghm  19286  ghmeql  19309  iscmn  19859  isomnd  20193  rnghmval  20522  dfrhm2  20556  zrrnghm  20621  isorng  20942  islss  21033  lssacs  21066  lmhmeql  21154  islbs  21175  lbsextlem1  21260  lbsextlem3  21262  lbsextlem4  21263  isobs  21839  mat0dimcrng  22596  istopg  23021  isbasisg  23073  basis2  23077  eltg2  23084  iscldtop  23221  neipeltop  23255  isreg  23458  regsep  23460  isnrm  23461  islly  23594  isnlly  23595  llyi  23600  nllyi  23601  islly2  23610  cldllycmp  23621  isfbas  23955  fbssfi  23963  isust  24330  elutop  24359  ustuqtop  24372  utopsnneip  24374  ispsmet  24430  ismet  24449  isxmet  24450  metrest  24650  cncfval  25016  fmcfil  25400  iscfil3  25401  caucfil  25411  iscmet3  25421  cfilres  25424  minveclem3  25557  wilthlem2  27199  wilthlem3  27200  wilth  27201  dfn0s2  28491  dfconngr1  30480  isconngr  30481  1conngr  30486  isplig  30769  isgrpo  30790  isablo  30839  disjabrex  32868  disjabrexf  32869  isrnsiga  34448  isldsys  34491  isros  34503  issros  34510  bnj1286  35352  bnj1452  35385  kur14lem9  35639  cvmscbv  35683  cvmsi  35690  cvmsval  35691  nmulprop  36615  neibastop1  36793  neibastop2lem  36794  neibastop2  36795  dfttc4lem1  36962  rdgssun  37946  isbnd  38353  ismndo2  38447  rngomndo  38508  isidl  38587  ispsubsp  40443  sn-isghm  43331  isnacs  43361  mzpclval  43382  elmzpcl  43383  relpeq4  45582  permac8prim  45649  nelsubc3lem  49767  isthinc  50116