Theorem intss1 4913

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 3440	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4903	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2819	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2820	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3551	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3940	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2111   ⊆ wss 3902  ∩ cint 4897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-int 4898

This theorem is referenced by:  intminss  4924  intmin3  4926  intab  4928  int0el  4929  trintss  5216  intex  5282  intidg  5398  oneqmini  6359  sorpssint  7666  onint  7723  onssmin  7725  onnmin  7731  nnawordex  8552  cofon1  8587  cofonr  8589  dffi2  9307  inficl  9309  dffi3  9315  tcmin  9631  tc2  9632  rankr1ai  9688  rankuni2b  9743  tcrank  9774  harval2  9887  cfflb  10147  fin23lem20  10225  fin23lem38  10237  isf32lem2  10242  intwun  10623  inttsk  10662  intgru  10702  dfnn2  12135  dfuzi  12561  trclubi  14900  trclubgi  14901  trclub  14902  trclubg  14903  cotrtrclfv  14916  trclun  14918  dfrtrcl2  14966  mremre  17503  isacs1i  17560  mrelatglb  18463  cycsubg  19118  efgrelexlemb  19660  efgcpbllemb  19665  frgpuplem  19682  rgspnmin  20528  primefld  20718  cssmre  21628  toponmre  23006  1stcfb  23358  ptcnplem  23534  fbssfi  23750  uffix  23834  ufildom1  23839  alexsublem  23957  alexsubALTlem4  23963  tmdgsum2  24009  bcth3  25256  limciun  25820  aalioulem3  26267  sltval2  27593  sltres  27599  nocvxminlem  27715  eqscut2  27745  scutun12  27749  scutbdaybnd  27754  scutbdaybnd2  27755  scutbdaylt  27757  madebdaylemlrcut  27842  cofcut1  27862  cofcutr  27866  dfn0s2  28258  shintcli  31304  shsval2i  31362  ococin  31383  chsupsn  31388  elrgspnlem4  33207  fldgensdrg  33275  fldgenssv  33276  fldgenssp  33279  insiga  34145  ldsysgenld  34168  ldgenpisyslem2  34172  mclsssvlem  35594  mclsax  35601  mclsind  35602  untint  35744  dfon2lem8  35823  dfon2lem9  35824  clsint2  36362  topmeet  36397  topjoin  36398  heibor1lem  37848  ismrcd1  42730  mzpincl  42766  mzpf  42768  mzpindd  42778  onintunirab  43259  oninfint  43268  clublem  43642  dftrcl3  43752  brtrclfv2  43759  dfrtrcl3  43765  intsaluni  46366  intsal  46367  salgenss  46373  salgencntex  46380  intubeu  49014