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

Syntax hints:   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ⊆ wss 3898  ∩ 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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-int 4898

This theorem is referenced by:  intminss  4924  intmin3  4926  intab  4928  int0el  4929  trintss  5218  intex  5284  intidg  5400  oneqmini  6364  sorpssint  7672  onint  7729  onssmin  7731  onnmin  7737  nnawordex  8558  cofon1  8593  cofonr  8595  dffi2  9314  inficl  9316  dffi3  9322  tcmin  9636  tc2  9637  rankr1ai  9698  rankuni2b  9753  tcrank  9784  harval2  9897  cfflb  10157  fin23lem20  10235  fin23lem38  10247  isf32lem2  10252  intwun  10633  inttsk  10672  intgru  10712  dfnn2  12145  dfuzi  12570  trclubi  14905  trclubgi  14906  trclub  14907  trclubg  14908  cotrtrclfv  14921  trclun  14923  dfrtrcl2  14971  mremre  17508  isacs1i  17565  mrelatglb  18468  cycsubg  19122  efgrelexlemb  19664  efgcpbllemb  19669  frgpuplem  19686  rgspnmin  20532  primefld  20722  cssmre  21632  toponmre  23009  1stcfb  23361  ptcnplem  23537  fbssfi  23753  uffix  23837  ufildom1  23842  alexsublem  23960  alexsubALTlem4  23966  tmdgsum2  24012  bcth3  25259  limciun  25823  aalioulem3  26270  sltval2  27596  sltres  27602  nocvxminlem  27718  eqscut2  27748  scutun12  27752  scutbdaybnd  27757  scutbdaybnd2  27758  scutbdaylt  27760  madebdaylemlrcut  27845  cofcut1  27865  cofcutr  27869  dfn0s2  28261  shintcli  31311  shsval2i  31369  ococin  31390  chsupsn  31395  elrgspnlem4  33219  fldgensdrg  33287  fldgenssv  33288  fldgenssp  33291  insiga  34171  ldsysgenld  34194  ldgenpisyslem2  34198  mclsssvlem  35627  mclsax  35634  mclsind  35635  untint  35777  dfon2lem8  35853  dfon2lem9  35854  clsint2  36394  topmeet  36429  topjoin  36430  heibor1lem  37869  ismrcd1  42815  mzpincl  42851  mzpf  42853  mzpindd  42863  onintunirab  43344  oninfint  43353  clublem  43727  dftrcl3  43837  brtrclfv2  43844  dfrtrcl3  43850  intsaluni  46451  intsal  46452  salgenss  46458  salgencntex  46465  intubeu  49108