Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  intss1 Structured version   Visualization version   GIF version

Theorem intss1 4427
 Description: An element of a class includes the intersection of the class. Exercise 4 of [TakeutiZaring] p. 44 (with correction), generalized to classes. (Contributed by NM, 18-Nov-1995.)
Assertion
Ref Expression
intss1 (𝐴𝐵 𝐵𝐴)

Proof of Theorem intss1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 3176 . . . 4 𝑥 ∈ V
21elint 4416 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2676 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2677 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 333 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3266 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 52 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7syl5bi 231 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3574 1 (𝐴𝐵 𝐵𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ⊆ wss 3540  ∩ cint 4410 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-13 2234  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-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-int 4411 This theorem is referenced by:  intminss  4438  intmin3  4440  intab  4442  int0el  4443  trint0  4698  intex  4747  oneqmini  5693  sorpssint  6845  onint  6887  onssmin  6889  onnmin  6895  nnawordex  7604  dffi2  8212  inficl  8214  dffi3  8220  tcmin  8500  tc2  8501  rankr1ai  8544  rankuni2b  8599  tcrank  8630  harval2  8706  cfflb  8964  fin23lem20  9042  fin23lem38  9054  isf32lem2  9059  intwun  9436  inttsk  9475  intgru  9515  dfnn2  10910  dfuzi  11344  trclubi  13583  trclubiOLD  13584  trclubgi  13585  trclubgiOLD  13586  trclub  13587  trclubg  13588  cotrtrclfv  13601  trclun  13603  dfrtrcl2  13650  mremre  16087  isacs1i  16141  mrelatglb  17007  cycsubg  17445  efgrelexlemb  17986  efgcpbllemb  17991  frgpuplem  18008  cssmre  19856  toponmre  20707  1stcfb  21058  ptcnplem  21234  fbssfi  21451  uffix  21535  ufildom1  21540  alexsublem  21658  alexsubALTlem4  21664  tmdgsum2  21710  bcth3  22936  limciun  23464  aalioulem3  23893  shintcli  27572  shsval2i  27630  ococin  27651  chsupsn  27656  insiga  29527  ldsysgenld  29550  ldgenpisyslem2  29554  mclsssvlem  30713  mclsax  30720  mclsind  30721  untint  30843  dfon2lem8  30939  dfon2lem9  30940  sltval2  31053  sltres  31061  nodenselem7  31086  nocvxminlem  31089  nobndup  31099  nobnddown  31100  clsint2  31494  topmeet  31529  topjoin  31530  heibor1lem  32778  ismrcd1  36279  mzpincl  36315  mzpf  36317  mzpindd  36327  rgspnmin  36760  clublem  36936  dftrcl3  37031  brtrclfv2  37038  dfrtrcl3  37044  intsaluni  39223  intsal  39224  salgenss  39230  salgencntex  39237
 Copyright terms: Public domain W3C validator