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

Theorem intss1 4882
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 3495 . . . 4 𝑥 ∈ V
21elint 4873 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2897 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2898 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 346 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3592 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 54 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7syl5bi 243 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3970 1 (𝐴𝐵 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526   = wceq 1528  wcel 2105  wss 3933   cint 4867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-int 4868
This theorem is referenced by:  intminss  4893  intmin3  4895  intab  4897  int0el  4898  trintss  5180  intex  5231  oneqmini  6235  sorpssint  7448  onint  7499  onssmin  7501  onnmin  7507  nnawordex  8252  dffi2  8875  inficl  8877  dffi3  8883  tcmin  9171  tc2  9172  rankr1ai  9215  rankuni2b  9270  tcrank  9301  harval2  9414  cfflb  9669  fin23lem20  9747  fin23lem38  9759  isf32lem2  9764  intwun  10145  inttsk  10184  intgru  10224  dfnn2  11639  dfuzi  12061  trclubi  14344  trclubgi  14345  trclub  14346  trclubg  14347  cotrtrclfv  14360  trclun  14362  dfrtrcl2  14409  mremre  16863  isacs1i  16916  mrelatglb  17782  cycsubg  18289  efgrelexlemb  18805  efgcpbllemb  18810  frgpuplem  18827  primefld  19513  cssmre  20765  toponmre  21629  1stcfb  21981  ptcnplem  22157  fbssfi  22373  uffix  22457  ufildom1  22462  alexsublem  22580  alexsubALTlem4  22586  tmdgsum2  22632  bcth3  23861  limciun  24419  aalioulem3  24850  shintcli  29033  shsval2i  29091  ococin  29112  chsupsn  29117  insiga  31295  ldsysgenld  31318  ldgenpisyslem2  31322  mclsssvlem  32706  mclsax  32713  mclsind  32714  untint  32835  dfon2lem8  32932  dfon2lem9  32933  sltval2  33060  sltres  33066  nocvxminlem  33144  scutun12  33168  scutbdaybnd  33172  scutbdaylt  33173  clsint2  33574  topmeet  33609  topjoin  33610  heibor1lem  34968  ismrcd1  39173  mzpincl  39209  mzpf  39211  mzpindd  39221  rgspnmin  39649  clublem  39848  dftrcl3  39943  brtrclfv2  39950  dfrtrcl3  39956  intsaluni  42489  intsal  42490  salgenss  42496  salgencntex  42503
  Copyright terms: Public domain W3C validator