Theorem intss1 4905

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 3433	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4895	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2824	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2825	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3538	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3927	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ⊆ wss 3889  ∩ cint 4889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-int 4890

This theorem is referenced by:  intminss  4916  intmin3  4918  intab  4920  int0el  4921  trintss  5211  intex  5285  intidg  5409  oneqmini  6376  sorpssint  7687  onint  7744  onssmin  7746  onnmin  7752  nnawordex  8573  cofon1  8608  cofonr  8610  dffi2  9336  inficl  9338  dffi3  9344  tcmin  9660  tc2  9661  rankr1ai  9722  rankuni2b  9777  tcrank  9808  harval2  9921  cfflb  10181  fin23lem20  10259  fin23lem38  10271  isf32lem2  10276  intwun  10658  inttsk  10697  intgru  10737  dfnn2  12187  dfuzi  12620  trclubi  14958  trclubgi  14959  trclub  14960  trclubg  14961  cotrtrclfv  14974  trclun  14976  dfrtrcl2  15024  mremre  17566  isacs1i  17623  mrelatglb  18526  cycsubg  19183  efgrelexlemb  19725  efgcpbllemb  19730  frgpuplem  19747  rgspnmin  20592  primefld  20782  cssmre  21673  toponmre  23058  1stcfb  23410  ptcnplem  23586  fbssfi  23802  uffix  23886  ufildom1  23891  alexsublem  24009  alexsubALTlem4  24015  tmdgsum2  24061  bcth3  25298  limciun  25861  aalioulem3  26300  ltsval2  27620  ltsres  27626  nocvxminlem  27746  eqcuts2  27778  cutsun12  27782  cutbdaybnd  27787  cutbdaybnd2  27788  cutbdaylt  27790  madebdaylemlrcut  27891  sltsbday  27909  cofcut1  27912  cofcutr  27916  addonbday  28271  dfn0s2  28324  shintcli  31400  shsval2i  31458  ococin  31479  chsupsn  31484  elrgspnlem4  33306  fldgensdrg  33375  fldgenssv  33376  fldgenssp  33379  insiga  34281  ldsysgenld  34304  ldgenpisyslem2  34308  mclsssvlem  35744  mclsax  35751  mclsind  35752  untint  35894  dfon2lem8  35970  dfon2lem9  35971  clsint2  36511  topmeet  36546  topjoin  36547  heibor1lem  38130  ismrcd1  43130  mzpincl  43166  mzpf  43168  mzpindd  43178  onintunirab  43655  oninfint  43664  clublem  44037  dftrcl3  44147  brtrclfv2  44154  dfrtrcl3  44160  intsaluni  46757  intsal  46758  salgenss  46764  salgencntex  46771  intubeu  49459