Theorem intss1 4968

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 3476	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4957	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2819	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2820	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 343	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3587	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 241	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3989	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1537   = wceq 1539   ∈ wcel 2104   ⊆ wss 3949  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-int 4952

This theorem is referenced by:  intminss  4979  intmin3  4981  intab  4983  int0el  4984  trintss  5285  intex  5338  intidg  5458  oneqmini  6417  sorpssint  7727  onint  7782  onssmin  7784  onnmin  7790  nnawordex  8641  cofon1  8675  cofonr  8677  dffi2  9422  inficl  9424  dffi3  9430  tcmin  9740  tc2  9741  rankr1ai  9797  rankuni2b  9852  tcrank  9883  harval2  9996  cfflb  10258  fin23lem20  10336  fin23lem38  10348  isf32lem2  10353  intwun  10734  inttsk  10773  intgru  10813  dfnn2  12231  dfuzi  12659  trclubi  14949  trclubgi  14950  trclub  14951  trclubg  14952  cotrtrclfv  14965  trclun  14967  dfrtrcl2  15015  mremre  17554  isacs1i  17607  mrelatglb  18519  cycsubg  19125  efgrelexlemb  19661  efgcpbllemb  19666  frgpuplem  19683  primefld  20566  cssmre  21467  toponmre  22819  1stcfb  23171  ptcnplem  23347  fbssfi  23563  uffix  23647  ufildom1  23652  alexsublem  23770  alexsubALTlem4  23776  tmdgsum2  23822  bcth3  25081  limciun  25645  aalioulem3  26081  sltval2  27393  sltres  27399  nocvxminlem  27513  eqscut2  27542  scutun12  27546  scutbdaybnd  27551  scutbdaybnd2  27552  scutbdaylt  27554  madebdaylemlrcut  27628  cofcut1  27643  cofcutr  27647  dfn0s2  27939  shintcli  30847  shsval2i  30905  ococin  30926  chsupsn  30931  fldgensdrg  32672  fldgenssv  32673  fldgenssp  32676  insiga  33431  ldsysgenld  33454  ldgenpisyslem2  33458  mclsssvlem  34849  mclsax  34856  mclsind  34857  untint  34983  dfon2lem8  35064  dfon2lem9  35065  clsint2  35519  topmeet  35554  topjoin  35555  heibor1lem  36982  ismrcd1  41740  mzpincl  41776  mzpf  41778  mzpindd  41788  rgspnmin  42217  onintunirab  42280  oninfint  42289  clublem  42665  dftrcl3  42775  brtrclfv2  42782  dfrtrcl3  42788  intsaluni  45345  intsal  45346  salgenss  45352  salgencntex  45359  intubeu  47698