Theorem intss1 4894

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.

Step	Hyp	Ref	Expression
1		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4885	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2826	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2827	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3535	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 241	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3927	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1537   = wceq 1539   ∈ wcel 2106   ⊆ wss 3887  ∩ cint 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-int 4880

This theorem is referenced by:  intminss  4905  intmin3  4907  intab  4909  int0el  4910  trintss  5208  intex  5261  oneqmini  6317  sorpssint  7586  onint  7640  onssmin  7642  onnmin  7648  nnawordex  8468  dffi2  9182  inficl  9184  dffi3  9190  tcmin  9499  tc2  9500  rankr1ai  9556  rankuni2b  9611  tcrank  9642  harval2  9755  cfflb  10015  fin23lem20  10093  fin23lem38  10105  isf32lem2  10110  intwun  10491  inttsk  10530  intgru  10570  dfnn2  11986  dfuzi  12411  trclubi  14707  trclubgi  14708  trclub  14709  trclubg  14710  cotrtrclfv  14723  trclun  14725  dfrtrcl2  14773  mremre  17313  isacs1i  17366  mrelatglb  18278  cycsubg  18827  efgrelexlemb  19356  efgcpbllemb  19361  frgpuplem  19378  primefld  20073  cssmre  20898  toponmre  22244  1stcfb  22596  ptcnplem  22772  fbssfi  22988  uffix  23072  ufildom1  23077  alexsublem  23195  alexsubALTlem4  23201  tmdgsum2  23247  bcth3  24495  limciun  25058  aalioulem3  25494  shintcli  29691  shsval2i  29749  ococin  29770  chsupsn  29775  insiga  32105  ldsysgenld  32128  ldgenpisyslem2  32132  mclsssvlem  33524  mclsax  33531  mclsind  33532  untint  33653  dfon2lem8  33766  dfon2lem9  33767  sltval2  33859  sltres  33865  nocvxminlem  33972  eqscut2  34000  scutun12  34004  scutbdaybnd  34009  scutbdaybnd2  34010  scutbdaylt  34012  madebdaylemlrcut  34079  cofcut1  34090  cofcutr  34092  clsint2  34518  topmeet  34553  topjoin  34554  heibor1lem  35967  ismrcd1  40520  mzpincl  40556  mzpf  40558  mzpindd  40568  rgspnmin  40996  clublem  41218  dftrcl3  41328  brtrclfv2  41335  dfrtrcl3  41341  intsaluni  43868  intsal  43869  salgenss  43875  salgencntex  43882  intubeu  46270