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

Theorem intss1 4421
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 3175 . . . 4 𝑥 ∈ V
21elint 4410 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2675 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2676 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 332 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3265 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 51 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7syl5bi 230 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3573 1 (𝐴𝐵 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472   = wceq 1474  wcel 1976  wss 3539   cint 4404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-int 4405
This theorem is referenced by:  intminss  4432  intmin3  4434  intab  4436  int0el  4437  trint0  4692  intex  4742  oneqmini  5679  sorpssint  6823  onint  6865  onssmin  6867  onnmin  6873  nnawordex  7582  dffi2  8190  inficl  8192  dffi3  8198  tcmin  8478  tc2  8479  rankr1ai  8522  rankuni2b  8577  tcrank  8608  harval2  8684  cfflb  8942  fin23lem20  9020  fin23lem38  9032  isf32lem2  9037  intwun  9414  inttsk  9453  intgru  9493  dfnn2  10883  dfuzi  11303  trclubi  13532  trclubiOLD  13533  trclubgi  13534  trclubgiOLD  13535  trclub  13536  trclubg  13537  cotrtrclfv  13550  trclun  13552  dfrtrcl2  13599  mremre  16036  isacs1i  16090  mrelatglb  16956  cycsubg  17394  efgrelexlemb  17935  efgcpbllemb  17940  frgpuplem  17957  cssmre  19804  toponmre  20655  1stcfb  21006  ptcnplem  21182  fbssfi  21399  uffix  21483  ufildom1  21488  alexsublem  21606  alexsubALTlem4  21612  tmdgsum2  21658  bcth3  22881  limciun  23409  aalioulem3  23838  shintcli  27406  shsval2i  27464  ococin  27485  chsupsn  27490  insiga  29361  ldsysgenld  29384  ldgenpisyslem2  29388  mclsssvlem  30547  mclsax  30554  mclsind  30555  untint  30677  dfon2lem8  30773  dfon2lem9  30774  sltval2  30887  sltres  30895  nodenselem7  30920  nocvxminlem  30923  nobndup  30933  nobnddown  30934  clsint2  31328  topmeet  31363  topjoin  31364  heibor1lem  32602  ismrcd1  36103  mzpincl  36139  mzpf  36141  mzpindd  36151  rgspnmin  36584  clublem  36760  dftrcl3  36855  brtrclfv2  36862  dfrtrcl3  36868  intsaluni  39047  intsal  39048  salgenss  39054  salgencntex  39061
  Copyright terms: Public domain W3C validator