Theorem intss1 4891

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 3426	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4882	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2826	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2827	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3525	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 241	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3923	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1537   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-int 4877

This theorem is referenced by:  intminss  4902  intmin3  4904  intab  4906  int0el  4907  trintss  5204  intex  5256  oneqmini  6302  sorpssint  7564  onint  7617  onssmin  7619  onnmin  7625  nnawordex  8430  dffi2  9112  inficl  9114  dffi3  9120  tcmin  9430  tc2  9431  rankr1ai  9487  rankuni2b  9542  tcrank  9573  harval2  9686  cfflb  9946  fin23lem20  10024  fin23lem38  10036  isf32lem2  10041  intwun  10422  inttsk  10461  intgru  10501  dfnn2  11916  dfuzi  12341  trclubi  14635  trclubgi  14636  trclub  14637  trclubg  14638  cotrtrclfv  14651  trclun  14653  dfrtrcl2  14701  mremre  17230  isacs1i  17283  mrelatglb  18193  cycsubg  18742  efgrelexlemb  19271  efgcpbllemb  19276  frgpuplem  19293  primefld  19988  cssmre  20810  toponmre  22152  1stcfb  22504  ptcnplem  22680  fbssfi  22896  uffix  22980  ufildom1  22985  alexsublem  23103  alexsubALTlem4  23109  tmdgsum2  23155  bcth3  24400  limciun  24963  aalioulem3  25399  shintcli  29592  shsval2i  29650  ococin  29671  chsupsn  29676  insiga  32005  ldsysgenld  32028  ldgenpisyslem2  32032  mclsssvlem  33424  mclsax  33431  mclsind  33432  untint  33553  dfon2lem8  33672  dfon2lem9  33673  sltval2  33786  sltres  33792  nocvxminlem  33899  eqscut2  33927  scutun12  33931  scutbdaybnd  33936  scutbdaybnd2  33937  scutbdaylt  33939  madebdaylemlrcut  34006  cofcut1  34017  cofcutr  34019  clsint2  34445  topmeet  34480  topjoin  34481  heibor1lem  35894  ismrcd1  40436  mzpincl  40472  mzpf  40474  mzpindd  40484  rgspnmin  40912  clublem  41107  dftrcl3  41217  brtrclfv2  41224  dfrtrcl3  41230  intsaluni  43758  intsal  43759  salgenss  43765  salgencntex  43772  intubeu  46158