Theorem intss1 4900

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 3436	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4890	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2828	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2829	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3541	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 243	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3928	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1545   = wceq 1547   ∈ wcel 2119   ⊆ wss 3890  ∩ cint 4884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-int 4885

This theorem is referenced by:  intminss  4911  intmin3  4913  intab  4915  int0el  4916  trintss  5205  intex  5279  intidg  5403  oneqmini  6370  sorpssint  7683  onint  7740  onssmin  7742  onnmin  7748  nnawordex  8570  cofon1  8605  cofonr  8607  dffi2  9333  inficl  9335  dffi3  9341  tcmin  9658  tc2  9659  rankr1ai  9720  rankuni2b  9775  tcrank  9806  harval2  9919  cfflb  10179  fin23lem20  10257  fin23lem38  10269  isf32lem2  10274  intwun  10656  inttsk  10695  intgru  10735  dfnn2  12185  dfuzi  12618  trclubi  14956  trclubgi  14957  trclub  14958  trclubg  14959  cotrtrclfv  14972  trclun  14974  dfrtrcl2  15022  mremre  17564  isacs1i  17621  mrelatglb  18524  cycsubg  19181  efgrelexlemb  19723  efgcpbllemb  19728  frgpuplem  19745  rgspnmin  20594  primefld  20784  cssmre  21675  toponmre  23083  1stcfb  23435  ptcnplem  23611  fbssfi  23827  uffix  23911  ufildom1  23916  alexsublem  24034  alexsubALTlem4  24040  tmdgsum2  24086  bcth3  25323  limciun  25886  aalioulem3  26325  ltsval2  27645  ltsres  27651  nocvxminlem  27771  eqcuts2  27803  cutsun12  27807  cutbdaybnd  27812  cutbdaybnd2  27813  cutbdaylt  27815  madebdaylemlrcut  27916  sltsbday  27934  cofcut1  27937  cofcutr  27941  addonbday  28296  dfn0s2  28349  shintcli  31425  shsval2i  31483  ococin  31504  chsupsn  31509  elrgspnlem4  33333  fldgensdrg  33405  fldgenssv  33406  fldgenssp  33409  insiga  34328  ldsysgenld  34351  ldgenpisyslem2  34355  mclsssvlem  35797  mclsax  35804  mclsind  35805  untint  35947  dfon2lem8  36023  dfon2lem9  36024  clsint2  36564  topmeet  36599  topjoin  36600  heibor1lem  38183  ismrcd1  43154  mzpincl  43190  mzpf  43192  mzpindd  43202  onintunirab  43679  oninfint  43688  clublem  44061  dftrcl3  44171  brtrclfv2  44178  dfrtrcl3  44184  intsaluni  46779  intsal  46780  salgenss  46786  salgencntex  46793  intubeu  49481