Theorem raleqbi1dv 3146

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Hypothesis

Ref	Expression
raleqd.1	⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
raleqbi1dv	⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqbi1dv

Step	Hyp	Ref	Expression
1		raleq 3138	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
2		raleqd.1	. . 3 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	2	ralbidv 2986	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
4	1, 3	bitrd 268	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  ∀wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  isoeq4  6570  wfrlem1  7414  wfrlem4  7418  wfrlem15  7429  smo11  7461  dffi2  8329  inficl  8331  dffi3  8337  dfom3  8544  aceq1  8940  dfac5lem4  8949  kmlem1  8972  kmlem10  8981  kmlem13  8984  kmlem14  8985  cofsmo  9091  infpssrlem4  9128  axdc3lem2  9273  elwina  9508  elina  9509  iswun  9526  eltskg  9572  elgrug  9614  elnp  9809  elnpi  9810  dfnn2  11033  dfnn3  11034  dfuzi  11468  coprmprod  15375  coprmproddvds  15377  ismri  16291  isprs  16930  isdrs  16934  ispos  16947  istos  17035  pospropd  17134  isipodrs  17161  isdlat  17193  mhmpropd  17341  issubm  17347  subgacs  17629  nsgacs  17630  isghm  17660  ghmeql  17683  iscmn  18200  dfrhm2  18717  islss  18935  lssacs  18967  lmhmeql  19055  islbs  19076  lbsextlem1  19158  lbsextlem3  19160  lbsextlem4  19161  isobs  20064  mat0dimcrng  20276  istopg  20700  isbasisg  20751  basis2  20755  eltg2  20762  iscldtop  20899  neipeltop  20933  isreg  21136  regsep  21138  isnrm  21139  islly  21271  isnlly  21272  llyi  21277  nllyi  21278  islly2  21287  cldllycmp  21298  isfbas  21633  fbssfi  21641  isust  22007  elutop  22037  ustuqtop  22050  utopsnneip  22052  ispsmet  22109  ismet  22128  isxmet  22129  metrest  22329  cncfval  22691  fmcfil  23070  iscfil3  23071  caucfil  23081  iscmet3  23091  cfilres  23094  minveclem3  23200  wilthlem2  24795  wilthlem3  24796  wilth  24797  dfconngr1  27048  isconngr  27049  isplig  27328  isgrpo  27351  isablo  27400  disjabrex  29395  disjabrexf  29396  isomnd  29701  isorng  29799  isrnsigaOLD  30175  isrnsiga  30176  isldsys  30219  isros  30231  issros  30238  bnj1286  31087  bnj1452  31120  kur14lem9  31196  cvmscbv  31240  cvmsi  31247  cvmsval  31248  frrlem1  31780  frrlem4  31783  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  isbnd  33579  ismndo2  33673  rngomndo  33734  isidl  33813  ispsubsp  35031  isnacs  37267  mzpclval  37288  elmzpcl  37289  mgmhmpropd  41785  issubmgm  41789  rnghmval  41891  zrrnghm  41917