Theorem intss1 4939

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 3463	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4928	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2823	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3575	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3964	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1538   = wceq 1540   ∈ wcel 2108   ⊆ wss 3926  ∩ cint 4922

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-int 4923

This theorem is referenced by:  intminss  4950  intmin3  4952  intab  4954  int0el  4955  trintss  5248  intex  5314  intidg  5432  oneqmini  6405  sorpssint  7725  onint  7782  onssmin  7784  onnmin  7790  nnawordex  8647  cofon1  8682  cofonr  8684  dffi2  9433  inficl  9435  dffi3  9441  tcmin  9753  tc2  9754  rankr1ai  9810  rankuni2b  9865  tcrank  9896  harval2  10009  cfflb  10271  fin23lem20  10349  fin23lem38  10361  isf32lem2  10366  intwun  10747  inttsk  10786  intgru  10826  dfnn2  12251  dfuzi  12682  trclubi  15013  trclubgi  15014  trclub  15015  trclubg  15016  cotrtrclfv  15029  trclun  15031  dfrtrcl2  15079  mremre  17614  isacs1i  17667  mrelatglb  18568  cycsubg  19189  efgrelexlemb  19729  efgcpbllemb  19734  frgpuplem  19751  rgspnmin  20573  primefld  20763  cssmre  21651  toponmre  23029  1stcfb  23381  ptcnplem  23557  fbssfi  23773  uffix  23857  ufildom1  23862  alexsublem  23980  alexsubALTlem4  23986  tmdgsum2  24032  bcth3  25281  limciun  25845  aalioulem3  26292  sltval2  27618  sltres  27624  nocvxminlem  27739  eqscut2  27768  scutun12  27772  scutbdaybnd  27777  scutbdaybnd2  27778  scutbdaylt  27780  madebdaylemlrcut  27854  cofcut1  27871  cofcutr  27875  dfn0s2  28253  shintcli  31256  shsval2i  31314  ococin  31335  chsupsn  31340  elrgspnlem4  33186  fldgensdrg  33254  fldgenssv  33255  fldgenssp  33258  insiga  34114  ldsysgenld  34137  ldgenpisyslem2  34141  mclsssvlem  35530  mclsax  35537  mclsind  35538  untint  35675  dfon2lem8  35754  dfon2lem9  35755  clsint2  36293  topmeet  36328  topjoin  36329  heibor1lem  37779  ismrcd1  42668  mzpincl  42704  mzpf  42706  mzpindd  42716  onintunirab  43198  oninfint  43207  clublem  43581  dftrcl3  43691  brtrclfv2  43698  dfrtrcl3  43704  intsaluni  46306  intsal  46307  salgenss  46313  salgencntex  46320  intubeu  48906