Theorem intss1 4874

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 3412	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4865	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2825	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2826	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 348	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3511	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3907	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1541   = wceq 1543   ∈ wcel 2110   ⊆ wss 3866  ∩ cint 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-int 4860

This theorem is referenced by:  intminss  4885  intmin3  4887  intab  4889  int0el  4890  trintss  5178  intex  5230  oneqmini  6264  sorpssint  7521  onint  7574  onssmin  7576  onnmin  7582  nnawordex  8365  dffi2  9039  inficl  9041  dffi3  9047  tcmin  9357  tc2  9358  rankr1ai  9414  rankuni2b  9469  tcrank  9500  harval2  9613  cfflb  9873  fin23lem20  9951  fin23lem38  9963  isf32lem2  9968  intwun  10349  inttsk  10388  intgru  10428  dfnn2  11843  dfuzi  12268  trclubi  14559  trclubgi  14560  trclub  14561  trclubg  14562  cotrtrclfv  14575  trclun  14577  dfrtrcl2  14625  mremre  17107  isacs1i  17160  mrelatglb  18066  cycsubg  18615  efgrelexlemb  19140  efgcpbllemb  19145  frgpuplem  19162  primefld  19849  cssmre  20655  toponmre  21990  1stcfb  22342  ptcnplem  22518  fbssfi  22734  uffix  22818  ufildom1  22823  alexsublem  22941  alexsubALTlem4  22947  tmdgsum2  22993  bcth3  24228  limciun  24791  aalioulem3  25227  shintcli  29410  shsval2i  29468  ococin  29489  chsupsn  29494  insiga  31817  ldsysgenld  31840  ldgenpisyslem2  31844  mclsssvlem  33237  mclsax  33244  mclsind  33245  untint  33366  dfon2lem8  33485  dfon2lem9  33486  sltval2  33596  sltres  33602  nocvxminlem  33709  eqscut2  33737  scutun12  33741  scutbdaybnd  33746  scutbdaybnd2  33747  scutbdaylt  33749  madebdaylemlrcut  33816  cofcut1  33827  cofcutr  33829  clsint2  34255  topmeet  34290  topjoin  34291  heibor1lem  35704  ismrcd1  40223  mzpincl  40259  mzpf  40261  mzpindd  40271  rgspnmin  40699  clublem  40894  dftrcl3  41005  brtrclfv2  41012  dfrtrcl3  41018  intsaluni  43543  intsal  43544  salgenss  43550  salgencntex  43557  intubeu  45943