Theorem raleqbi1dv 3123

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 3115	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
2		raleqd.1	. . 3 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	2	ralbidv 2969	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
4	1, 3	bitrd 267	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901

This theorem is referenced by:  isoeq4  6470  wfrlem1  7301  wfrlem4  7305  wfrlem15  7316  smo11  7348  dffi2  8212  inficl  8214  dffi3  8220  dfom3  8427  aceq1  8823  dfac5lem4  8832  kmlem1  8855  kmlem10  8864  kmlem13  8867  kmlem14  8868  cofsmo  8974  infpssrlem4  9011  axdc3lem2  9156  elwina  9387  elina  9388  iswun  9405  eltskg  9451  elgrug  9493  elnp  9688  elnpi  9689  dfnn2  10910  dfnn3  10911  dfuzi  11344  coprmprod  15213  coprmproddvds  15215  ismri  16114  isprs  16753  isdrs  16757  ispos  16770  istos  16858  pospropd  16957  isipodrs  16984  isdlat  17016  mhmpropd  17164  issubm  17170  subgacs  17452  nsgacs  17453  isghm  17483  ghmeql  17506  iscmn  18023  dfrhm2  18540  islss  18756  lssacs  18788  lmhmeql  18876  islbs  18897  lbsextlem1  18979  lbsextlem3  18981  lbsextlem4  18982  isobs  19883  mat0dimcrng  20095  istopg  20525  isbasisg  20562  basis2  20566  eltg2  20573  iscldtop  20709  neipeltop  20743  isreg  20946  regsep  20948  isnrm  20949  islly  21081  isnlly  21082  llyi  21087  nllyi  21088  islly2  21097  cldllycmp  21108  isfbas  21443  fbssfi  21451  isust  21817  elutop  21847  ustuqtop  21860  utopsnneip  21862  ispsmet  21919  ismet  21938  isxmet  21939  metrest  22139  cncfval  22499  fmcfil  22878  iscfil3  22879  caucfil  22889  iscmet3  22899  cfilres  22902  minveclem3  23008  wilthlem2  24595  wilthlem3  24596  wilth  24597  isfrgra  26517  isplig  26720  isgrpo  26735  isablo  26784  disjabrex  28777  disjabrexf  28778  isomnd  29032  isorng  29130  isrnsigaOLD  29502  isrnsiga  29503  isldsys  29546  isros  29558  issros  29565  bnj1286  30341  bnj1452  30374  kur14lem9  30450  cvmscbv  30494  cvmsi  30501  cvmsval  30502  frrlem1  31024  frrlem4  31027  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  isbnd  32749  ismndo2  32843  rngomndo  32904  isidl  32983  ispsubsp  34049  isnacs  36285  mzpclval  36306  elmzpcl  36307  dfconngr1  41355  mgmhmpropd  41575  issubmgm  41579  rnghmval  41681  zrrnghm  41707