Theorem intss1 4923

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 3455	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4913	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2849	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2850	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3551	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 55	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3937	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ⊆ wss 3899  ∩ cint 4907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-int 4908

This theorem is used by:  intminss  4934  intmin3  4936  intab  4938  int0el  4939  trintss  5231  intex  5305  intidg  5425  oneqmini  6409  sorpssint  7738  onint  7793  onssmin  7795  onnmin  7801  nnawordex  8630  cofon1  8665  cofonr  8667  dffi2  9399  inficl  9401  dffi3  9407  tcmin  9724  tc2  9725  rankr1ai  9788  rankuni2b  9848  tcrank  9882  harval2  10059  cfflb  10318  fin23lem20  10396  fin23lem38  10408  isf32lem2  10413  intwun  10801  inttsk  10840  intgru  10880  dfnn2  12329  dfuzi  12771  trclubi  15129  trclubgi  15130  trclub  15131  trclubg  15132  cotrtrclfv  15145  trclun  15147  dfrtrcl2  15195  mremre  17754  isacs1i  17811  mrelatglb  18714  cycsubg  19403  efgrelexlemb  19944  efgcpbllemb  19949  frgpuplem  19966  rgspnmin  20847  primefld  21042  cssmre  21979  toponmre  23391  1stcfb  23743  ptcnplem  23920  fbssfi  24136  uffix  24220  ufildom1  24225  alexsublem  24343  alexsubALTlem4  24349  tmdgsum2  24395  bcth3  25632  limciun  26194  aalioulem3  26643  ltsval2  27995  ltsres  28001  nocvxminlem  28122  eqcuts2  28154  cutsun12  28158  cutbdaybnd  28163  cutbdaybnd2  28164  cutbdaylt  28166  madebdaylemlrcut  28267  sltsbday  28285  cofcut1  28288  cofcutr  28292  addonbday  28647  dfn0s2  28700  shintcli  31913  shsval2i  31971  ococin  31992  chsupsn  31997  elrgspnlem4  33788  fldgensdrg  33858  fldgenssv  33859  fldgenssp  33862  insiga  34752  ldsysgenld  34775  ldgenpisyslem2  34779  fnfvintima  35695  dfscott3  35721  mclsssvlem  36296  mclsax  36303  mclsind  36304  untint  36446  dfon2lem8  36522  dfon2lem9  36523  clsint2  37087  topmeet  37122  topjoin  37123  heibor1lem  38711  ismrcd1  43662  mzpincl  43698  mzpf  43700  mzpindd  43710  onintunirab  44187  oninfint  44196  clublem  44569  dftrcl3  44679  brtrclfv2  44686  dfrtrcl3  44692  intsaluni  47283  intsal  47284  salgenss  47290  salgencntex  47297  intubeu  50036