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

Theorem intss1 4966
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 3478 . . . 4 𝑥 ∈ V
21elint 4955 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2821 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2822 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 344 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3586 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 54 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7biimtrid 241 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3987 1 (𝐴𝐵 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539   = wceq 1541  wcel 2106  wss 3947   cint 4949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-int 4950
This theorem is referenced by:  intminss  4977  intmin3  4979  intab  4981  int0el  4982  trintss  5283  intex  5336  intidg  5456  oneqmini  6413  sorpssint  7719  onint  7774  onssmin  7776  onnmin  7782  nnawordex  8633  cofon1  8667  cofonr  8669  dffi2  9414  inficl  9416  dffi3  9422  tcmin  9732  tc2  9733  rankr1ai  9789  rankuni2b  9844  tcrank  9875  harval2  9988  cfflb  10250  fin23lem20  10328  fin23lem38  10340  isf32lem2  10345  intwun  10726  inttsk  10765  intgru  10805  dfnn2  12221  dfuzi  12649  trclubi  14939  trclubgi  14940  trclub  14941  trclubg  14942  cotrtrclfv  14955  trclun  14957  dfrtrcl2  15005  mremre  17544  isacs1i  17597  mrelatglb  18509  cycsubg  19079  efgrelexlemb  19612  efgcpbllemb  19617  frgpuplem  19634  primefld  20413  cssmre  21237  toponmre  22588  1stcfb  22940  ptcnplem  23116  fbssfi  23332  uffix  23416  ufildom1  23421  alexsublem  23539  alexsubALTlem4  23545  tmdgsum2  23591  bcth3  24839  limciun  25402  aalioulem3  25838  sltval2  27148  sltres  27154  nocvxminlem  27268  eqscut2  27296  scutun12  27300  scutbdaybnd  27305  scutbdaybnd2  27306  scutbdaylt  27308  madebdaylemlrcut  27382  cofcut1  27396  cofcutr  27400  shintcli  30569  shsval2i  30627  ococin  30648  chsupsn  30653  fldgensdrg  32392  fldgenssv  32393  fldgenssp  32396  insiga  33123  ldsysgenld  33146  ldgenpisyslem2  33150  mclsssvlem  34541  mclsax  34548  mclsind  34549  untint  34669  dfon2lem8  34750  dfon2lem9  34751  clsint2  35202  topmeet  35237  topjoin  35238  heibor1lem  36665  ismrcd1  41421  mzpincl  41457  mzpf  41459  mzpindd  41469  rgspnmin  41898  onintunirab  41961  oninfint  41970  clublem  42346  dftrcl3  42456  brtrclfv2  42463  dfrtrcl3  42469  intsaluni  45031  intsal  45032  salgenss  45038  salgencntex  45045  intubeu  47562
  Copyright terms: Public domain W3C validator