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

Theorem intss1 4677
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 3390 . . . 4 𝑥 ∈ V
21elint 4668 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2869 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2870 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 335 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3482 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 54 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7syl5bi 233 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3798 1 (𝐴𝐵 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635   = wceq 1637  wcel 2155  wss 3763   cint 4662
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 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-v 3389  df-in 3770  df-ss 3777  df-int 4663
This theorem is referenced by:  intminss  4688  intmin3  4690  intab  4692  int0el  4693  trintss  4955  intex  5006  oneqmini  5983  sorpssint  7171  onint  7219  onssmin  7221  onnmin  7227  nnawordex  7948  dffi2  8562  inficl  8564  dffi3  8570  tcmin  8858  tc2  8859  rankr1ai  8902  rankuni2b  8957  tcrank  8988  harval2  9100  cfflb  9360  fin23lem20  9438  fin23lem38  9450  isf32lem2  9455  intwun  9836  inttsk  9875  intgru  9915  dfnn2  11312  dfuzi  11728  trclubi  13954  trclubgi  13955  trclub  13956  trclubg  13957  cotrtrclfv  13970  trclun  13972  dfrtrcl2  14019  mremre  16463  isacs1i  16516  mrelatglb  17383  cycsubg  17818  efgrelexlemb  18358  efgcpbllemb  18363  frgpuplem  18380  cssmre  20241  toponmre  21105  1stcfb  21456  ptcnplem  21632  fbssfi  21848  uffix  21932  ufildom1  21937  alexsublem  22055  alexsubALTlem4  22061  tmdgsum2  22107  bcth3  23334  limciun  23866  aalioulem3  24297  shintcli  28510  shsval2i  28568  ococin  28589  chsupsn  28594  insiga  30519  ldsysgenld  30542  ldgenpisyslem2  30546  mclsssvlem  31776  mclsax  31783  mclsind  31784  untint  31905  dfon2lem8  32009  dfon2lem9  32010  sltval2  32124  sltres  32130  nocvxminlem  32208  scutun12  32232  scutbdaybnd  32236  scutbdaylt  32237  clsint2  32639  topmeet  32674  topjoin  32675  heibor1lem  33913  ismrcd1  37757  mzpincl  37793  mzpf  37795  mzpindd  37805  rgspnmin  38236  clublem  38411  dftrcl3  38506  brtrclfv2  38513  dfrtrcl3  38519  intsaluni  41020  intsal  41021  salgenss  41027  salgencntex  41034
  Copyright terms: Public domain W3C validator