Theorem raleqbi1dv 3346

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ∀wral 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112

This theorem is referenced by:  isoeq4  6804  wfrlem1  7659  wfrlem4  7663  wfrlem4OLD  7664  wfrlem15  7675  smo11  7707  dffi2  8578  inficl  8580  dffi3  8586  dfom3  8801  aceq1  9233  dfac5lem4  9242  kmlem1  9267  kmlem10  9276  kmlem13  9279  kmlem14  9280  cofsmo  9386  infpssrlem4  9423  axdc3lem2  9568  elwina  9803  elina  9804  iswun  9821  eltskg  9867  elgrug  9909  elnp  10104  elnpi  10105  dfnn2  11330  dfnn3  11331  dfuzi  11754  coprmprod  15613  coprmproddvds  15615  ismri  16516  isprs  17155  isdrs  17159  ispos  17172  istos  17260  pospropd  17359  isipodrs  17386  isdlat  17418  mhmpropd  17566  issubm  17572  subgacs  17851  nsgacs  17852  isghm  17882  ghmeql  17905  iscmn  18421  dfrhm2  18941  islss  19159  lssacs  19194  lmhmeql  19282  islbs  19303  lbsextlem1  19387  lbsextlem3  19389  lbsextlem4  19390  isobs  20295  mat0dimcrng  20508  istopg  20934  isbasisg  20986  basis2  20990  eltg2  20997  iscldtop  21134  neipeltop  21168  isreg  21371  regsep  21373  isnrm  21374  islly  21506  isnlly  21507  llyi  21512  nllyi  21513  islly2  21522  cldllycmp  21533  isfbas  21867  fbssfi  21875  isust  22241  elutop  22271  ustuqtop  22284  utopsnneip  22286  ispsmet  22343  ismet  22362  isxmet  22363  metrest  22563  cncfval  22925  fmcfil  23304  iscfil3  23305  caucfil  23315  iscmet3  23325  cfilres  23328  minveclem3  23435  wilthlem2  25032  wilthlem3  25033  wilth  25034  dfconngr1  27384  isconngr  27385  isplig  27682  isgrpo  27703  isablo  27752  disjabrex  29743  disjabrexf  29744  isomnd  30049  isorng  30147  isrnsigaOLD  30523  isrnsiga  30524  isldsys  30567  isros  30579  issros  30586  bnj1286  31432  bnj1452  31465  kur14lem9  31541  cvmscbv  31585  cvmsi  31592  cvmsval  31593  frrlem1  32123  neibastop1  32697  neibastop2lem  32698  neibastop2  32699  isbnd  33909  ismndo2  34003  rngomndo  34064  isidl  34143  ispsubsp  35544  isnacs  37787  mzpclval  37808  elmzpcl  37809  mgmhmpropd  42371  issubmgm  42375  rnghmval  42477  zrrnghm  42503