Theorem intss1 4797

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 4788	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2870	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2871	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 346	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3538	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 243	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3895	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1520   = wceq 1522   ∈ wcel 2081   ⊆ wss 3859  ∩ cint 4782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3866  df-ss 3874  df-int 4783

This theorem is referenced by:  intminss  4808  intmin3  4810  intab  4812  int0el  4813  trintss  5080  intex  5131  oneqmini  6117  sorpssint  7317  onint  7366  onssmin  7368  onnmin  7374  nnawordex  8113  dffi2  8733  inficl  8735  dffi3  8741  tcmin  9029  tc2  9030  rankr1ai  9073  rankuni2b  9128  tcrank  9159  harval2  9272  cfflb  9527  fin23lem20  9605  fin23lem38  9617  isf32lem2  9622  intwun  10003  inttsk  10042  intgru  10082  dfnn2  11499  dfuzi  11922  trclubi  14190  trclubgi  14191  trclub  14192  trclubg  14193  cotrtrclfv  14206  trclun  14208  dfrtrcl2  14255  mremre  16704  isacs1i  16757  mrelatglb  17623  cycsubg  18061  efgrelexlemb  18603  efgcpbllemb  18608  frgpuplem  18625  primefld  19274  cssmre  20519  toponmre  21385  1stcfb  21737  ptcnplem  21913  fbssfi  22129  uffix  22213  ufildom1  22218  alexsublem  22336  alexsubALTlem4  22342  tmdgsum2  22388  bcth3  23617  limciun  24175  aalioulem3  24606  shintcli  28797  shsval2i  28855  ococin  28876  chsupsn  28881  insiga  31013  ldsysgenld  31036  ldgenpisyslem2  31040  mclsssvlem  32417  mclsax  32424  mclsind  32425  untint  32546  dfon2lem8  32643  dfon2lem9  32644  sltval2  32772  sltres  32778  nocvxminlem  32856  scutun12  32880  scutbdaybnd  32884  scutbdaylt  32885  clsint2  33286  topmeet  33321  topjoin  33322  heibor1lem  34619  ismrcd1  38780  mzpincl  38816  mzpf  38818  mzpindd  38828  rgspnmin  39256  clublem  39455  dftrcl3  39550  brtrclfv2  39557  dfrtrcl3  39563  intsaluni  42154  intsal  42155  salgenss  42161  salgencntex  42168