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

Theorem intss1 4963
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 3484 . . . 4 𝑥 ∈ V
21elint 4952 . . 3 (𝑥 𝐵 ↔ ∀𝑦(𝑦𝐵𝑥𝑦))
3 eleq1 2829 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐵𝐴𝐵))
4 eleq2 2830 . . . . . 6 (𝑦 = 𝐴 → (𝑥𝑦𝑥𝐴))
53, 4imbi12d 344 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐵𝑥𝑦) ↔ (𝐴𝐵𝑥𝐴)))
65spcgv 3596 . . . 4 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → (𝐴𝐵𝑥𝐴)))
76pm2.43a 54 . . 3 (𝐴𝐵 → (∀𝑦(𝑦𝐵𝑥𝑦) → 𝑥𝐴))
82, 7biimtrid 242 . 2 (𝐴𝐵 → (𝑥 𝐵𝑥𝐴))
98ssrdv 3989 1 (𝐴𝐵 𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538   = wceq 1540  wcel 2108  wss 3951   cint 4946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-int 4947
This theorem is referenced by:  intminss  4974  intmin3  4976  intab  4978  int0el  4979  trintss  5278  intex  5344  intidg  5462  oneqmini  6436  sorpssint  7753  onint  7810  onssmin  7812  onnmin  7818  nnawordex  8675  cofon1  8710  cofonr  8712  dffi2  9463  inficl  9465  dffi3  9471  tcmin  9781  tc2  9782  rankr1ai  9838  rankuni2b  9893  tcrank  9924  harval2  10037  cfflb  10299  fin23lem20  10377  fin23lem38  10389  isf32lem2  10394  intwun  10775  inttsk  10814  intgru  10854  dfnn2  12279  dfuzi  12709  trclubi  15035  trclubgi  15036  trclub  15037  trclubg  15038  cotrtrclfv  15051  trclun  15053  dfrtrcl2  15101  mremre  17647  isacs1i  17700  mrelatglb  18605  cycsubg  19226  efgrelexlemb  19768  efgcpbllemb  19773  frgpuplem  19790  rgspnmin  20615  primefld  20806  cssmre  21711  toponmre  23101  1stcfb  23453  ptcnplem  23629  fbssfi  23845  uffix  23929  ufildom1  23934  alexsublem  24052  alexsubALTlem4  24058  tmdgsum2  24104  bcth3  25365  limciun  25929  aalioulem3  26376  sltval2  27701  sltres  27707  nocvxminlem  27822  eqscut2  27851  scutun12  27855  scutbdaybnd  27860  scutbdaybnd2  27861  scutbdaylt  27863  madebdaylemlrcut  27937  cofcut1  27954  cofcutr  27958  dfn0s2  28336  shintcli  31348  shsval2i  31406  ococin  31427  chsupsn  31432  elrgspnlem4  33249  fldgensdrg  33316  fldgenssv  33317  fldgenssp  33320  insiga  34138  ldsysgenld  34161  ldgenpisyslem2  34165  mclsssvlem  35567  mclsax  35574  mclsind  35575  untint  35712  dfon2lem8  35791  dfon2lem9  35792  clsint2  36330  topmeet  36365  topjoin  36366  heibor1lem  37816  ismrcd1  42709  mzpincl  42745  mzpf  42747  mzpindd  42757  onintunirab  43239  oninfint  43248  clublem  43623  dftrcl3  43733  brtrclfv2  43740  dfrtrcl3  43746  intsaluni  46344  intsal  46345  salgenss  46351  salgencntex  46358  intubeu  48873
  Copyright terms: Public domain W3C validator