Theorem raleqbi1dv 3295

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066

This theorem is referenced by:  isoeq4  6716  wfrlem1  7570  wfrlem4  7574  wfrlem4OLD  7575  wfrlem15  7586  smo11  7618  dffi2  8489  inficl  8491  dffi3  8497  dfom3  8712  aceq1  9144  dfac5lem4  9153  kmlem1  9178  kmlem10  9187  kmlem13  9190  kmlem14  9191  cofsmo  9297  infpssrlem4  9334  axdc3lem2  9479  elwina  9714  elina  9715  iswun  9732  eltskg  9778  elgrug  9820  elnp  10015  elnpi  10016  dfnn2  11239  dfnn3  11240  dfuzi  11675  coprmprod  15582  coprmproddvds  15584  ismri  16499  isprs  17138  isdrs  17142  ispos  17155  istos  17243  pospropd  17342  isipodrs  17369  isdlat  17401  mhmpropd  17549  issubm  17555  subgacs  17837  nsgacs  17838  isghm  17868  ghmeql  17891  iscmn  18407  dfrhm2  18927  islss  19145  lssacs  19180  lmhmeql  19268  islbs  19289  lbsextlem1  19373  lbsextlem3  19375  lbsextlem4  19376  isobs  20281  mat0dimcrng  20494  istopg  20920  isbasisg  20972  basis2  20976  eltg2  20983  iscldtop  21120  neipeltop  21154  isreg  21357  regsep  21359  isnrm  21360  islly  21492  isnlly  21493  llyi  21498  nllyi  21499  islly2  21508  cldllycmp  21519  isfbas  21853  fbssfi  21861  isust  22227  elutop  22257  ustuqtop  22270  utopsnneip  22272  ispsmet  22329  ismet  22348  isxmet  22349  metrest  22549  cncfval  22911  fmcfil  23289  iscfil3  23290  caucfil  23300  iscmet3  23310  cfilres  23313  minveclem3  23419  wilthlem2  25016  wilthlem3  25017  wilth  25018  dfconngr1  27368  isconngr  27369  isplig  27670  isgrpo  27691  isablo  27740  disjabrex  29733  disjabrexf  29734  isomnd  30041  isorng  30139  isrnsigaOLD  30515  isrnsiga  30516  isldsys  30559  isros  30571  issros  30578  bnj1286  31425  bnj1452  31458  kur14lem9  31534  cvmscbv  31578  cvmsi  31585  cvmsval  31586  frrlem1  32117  neibastop1  32691  neibastop2lem  32692  neibastop2  32693  isbnd  33909  ismndo2  34003  rngomndo  34064  isidl  34143  ispsubsp  35552  isnacs  37791  mzpclval  37812  elmzpcl  37813  mgmhmpropd  42308  issubmgm  42312  rnghmval  42414  zrrnghm  42440