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

Theorem intss1 4853
 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 3444 . . . 4 𝑥 ∈ V
21elint 4844 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2877 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2878 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 348 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3543 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 54 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7syl5bi 245 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3921 1 (𝐴𝐵 𝐵𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ⊆ wss 3881  ∩ cint 4838 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-int 4839 This theorem is referenced by:  intminss  4864  intmin3  4866  intab  4868  int0el  4869  trintss  5153  intex  5204  oneqmini  6210  sorpssint  7441  onint  7492  onssmin  7494  onnmin  7500  nnawordex  8248  dffi2  8873  inficl  8875  dffi3  8881  tcmin  9169  tc2  9170  rankr1ai  9213  rankuni2b  9268  tcrank  9299  harval2  9412  cfflb  9672  fin23lem20  9750  fin23lem38  9762  isf32lem2  9767  intwun  10148  inttsk  10187  intgru  10227  dfnn2  11640  dfuzi  12063  trclubi  14349  trclubgi  14350  trclub  14351  trclubg  14352  cotrtrclfv  14365  trclun  14367  dfrtrcl2  14415  mremre  16869  isacs1i  16922  mrelatglb  17788  cycsubg  18346  efgrelexlemb  18871  efgcpbllemb  18876  frgpuplem  18893  primefld  19580  cssmre  20386  toponmre  21705  1stcfb  22057  ptcnplem  22233  fbssfi  22449  uffix  22533  ufildom1  22538  alexsublem  22656  alexsubALTlem4  22662  tmdgsum2  22708  bcth3  23942  limciun  24504  aalioulem3  24937  shintcli  29119  shsval2i  29177  ococin  29198  chsupsn  29203  insiga  31518  ldsysgenld  31541  ldgenpisyslem2  31545  mclsssvlem  32934  mclsax  32941  mclsind  32942  untint  33063  dfon2lem8  33160  dfon2lem9  33161  sltval2  33288  sltres  33294  nocvxminlem  33372  scutun12  33396  scutbdaybnd  33400  scutbdaylt  33401  clsint2  33802  topmeet  33837  topjoin  33838  heibor1lem  35263  ismrcd1  39654  mzpincl  39690  mzpf  39692  mzpindd  39702  rgspnmin  40130  clublem  40325  dftrcl3  40436  brtrclfv2  40443  dfrtrcl3  40449  intsaluni  42984  intsal  42985  salgenss  42991  salgencntex  42998
 Copyright terms: Public domain W3C validator