Theorem intss1 4906

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 3434	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4896	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2825	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2826	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3539	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3928	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ⊆ wss 3890  ∩ cint 4890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-int 4891

This theorem is referenced by:  intminss  4917  intmin3  4919  intab  4921  int0el  4922  trintss  5211  intex  5281  intidg  5404  oneqmini  6370  sorpssint  7680  onint  7737  onssmin  7739  onnmin  7745  nnawordex  8566  cofon1  8601  cofonr  8603  dffi2  9329  inficl  9331  dffi3  9337  tcmin  9651  tc2  9652  rankr1ai  9713  rankuni2b  9768  tcrank  9799  harval2  9912  cfflb  10172  fin23lem20  10250  fin23lem38  10262  isf32lem2  10267  intwun  10649  inttsk  10688  intgru  10728  dfnn2  12178  dfuzi  12611  trclubi  14949  trclubgi  14950  trclub  14951  trclubg  14952  cotrtrclfv  14965  trclun  14967  dfrtrcl2  15015  mremre  17557  isacs1i  17614  mrelatglb  18517  cycsubg  19174  efgrelexlemb  19716  efgcpbllemb  19721  frgpuplem  19738  rgspnmin  20583  primefld  20773  cssmre  21683  toponmre  23068  1stcfb  23420  ptcnplem  23596  fbssfi  23812  uffix  23896  ufildom1  23901  alexsublem  24019  alexsubALTlem4  24025  tmdgsum2  24071  bcth3  25308  limciun  25871  aalioulem3  26311  ltsval2  27634  ltsres  27640  nocvxminlem  27760  eqcuts2  27792  cutsun12  27796  cutbdaybnd  27801  cutbdaybnd2  27802  cutbdaylt  27804  madebdaylemlrcut  27905  sltsbday  27923  cofcut1  27926  cofcutr  27930  addonbday  28285  dfn0s2  28338  shintcli  31415  shsval2i  31473  ococin  31494  chsupsn  31499  elrgspnlem4  33321  fldgensdrg  33390  fldgenssv  33391  fldgenssp  33394  insiga  34297  ldsysgenld  34320  ldgenpisyslem2  34324  mclsssvlem  35760  mclsax  35767  mclsind  35768  untint  35910  dfon2lem8  35986  dfon2lem9  35987  clsint2  36527  topmeet  36562  topjoin  36563  heibor1lem  38144  ismrcd1  43144  mzpincl  43180  mzpf  43182  mzpindd  43192  onintunirab  43673  oninfint  43682  clublem  44055  dftrcl3  44165  brtrclfv2  44172  dfrtrcl3  44178  intsaluni  46775  intsal  46776  salgenss  46782  salgencntex  46789  intubeu  49471