Theorem intss1 4926

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 3457	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4916	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2850	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2851	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3553	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 55	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 245	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3940	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ⊆ wss 3902  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-int 4911

This theorem is used by:  intminss  4937  intmin3  4939  intab  4941  int0el  4942  trintss  5235  intex  5312  intidg  5436  oneqmini  6415  sorpssint  7738  onint  7793  onssmin  7795  onnmin  7801  nnawordex  8629  cofon1  8664  cofonr  8666  dffi2  9397  inficl  9399  dffi3  9405  tcmin  9722  tc2  9723  rankr1ai  9784  rankuni2b  9839  tcrank  9870  harval2  10006  cfflb  10265  fin23lem20  10343  fin23lem38  10355  isf32lem2  10360  intwun  10748  inttsk  10787  intgru  10827  dfnn2  12274  dfuzi  12716  trclubi  15073  trclubgi  15074  trclub  15075  trclubg  15076  cotrtrclfv  15089  trclun  15091  dfrtrcl2  15139  mremre  17694  isacs1i  17751  mrelatglb  18654  cycsubg  19342  efgrelexlemb  19883  efgcpbllemb  19888  frgpuplem  19905  rgspnmin  20783  primefld  20977  cssmre  21912  toponmre  23324  1stcfb  23676  ptcnplem  23853  fbssfi  24069  uffix  24153  ufildom1  24158  alexsublem  24276  alexsubALTlem4  24282  tmdgsum2  24328  bcth3  25565  limciun  26128  aalioulem3  26577  ltsval2  27900  ltsres  27906  nocvxminlem  28027  eqcuts2  28059  cutsun12  28063  cutbdaybnd  28068  cutbdaybnd2  28069  cutbdaylt  28071  madebdaylemlrcut  28172  sltsbday  28190  cofcut1  28193  cofcutr  28197  addonbday  28552  dfn0s2  28605  shintcli  31818  shsval2i  31876  ococin  31897  chsupsn  31902  elrgspnlem4  33693  fldgensdrg  33763  fldgenssv  33764  fldgenssp  33767  insiga  34656  ldsysgenld  34679  ldgenpisyslem2  34683  fnfvintima  35599  dfscott3  35634  mclsssvlem  36149  mclsax  36156  mclsind  36157  untint  36299  dfon2lem8  36375  dfon2lem9  36376  clsint2  36956  topmeet  36991  topjoin  36992  heibor1lem  38567  ismrcd1  43551  mzpincl  43587  mzpf  43589  mzpindd  43599  onintunirab  44076  oninfint  44085  clublem  44458  dftrcl3  44568  brtrclfv2  44575  dfrtrcl3  44581  intsaluni  47165  intsal  47166  salgenss  47172  salgencntex  47179  intubeu  49918