Theorem intss1 4967

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

Syntax hints:   → wi 4  ∀wal 1534   = wceq 1536   ∈ wcel 2105   ⊆ wss 3962  ∩ cint 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-int 4951

This theorem is referenced by:  intminss  4978  intmin3  4980  intab  4982  int0el  4983  trintss  5283  intex  5349  intidg  5467  oneqmini  6437  sorpssint  7751  onint  7809  onssmin  7811  onnmin  7817  nnawordex  8673  cofon1  8708  cofonr  8710  dffi2  9460  inficl  9462  dffi3  9468  tcmin  9778  tc2  9779  rankr1ai  9835  rankuni2b  9890  tcrank  9921  harval2  10034  cfflb  10296  fin23lem20  10374  fin23lem38  10386  isf32lem2  10391  intwun  10772  inttsk  10811  intgru  10851  dfnn2  12276  dfuzi  12706  trclubi  15031  trclubgi  15032  trclub  15033  trclubg  15034  cotrtrclfv  15047  trclun  15049  dfrtrcl2  15097  mremre  17648  isacs1i  17701  mrelatglb  18617  cycsubg  19238  efgrelexlemb  19782  efgcpbllemb  19787  frgpuplem  19804  rgspnmin  20631  primefld  20822  cssmre  21728  toponmre  23116  1stcfb  23468  ptcnplem  23644  fbssfi  23860  uffix  23944  ufildom1  23949  alexsublem  24067  alexsubALTlem4  24073  tmdgsum2  24119  bcth3  25378  limciun  25943  aalioulem3  26390  sltval2  27715  sltres  27721  nocvxminlem  27836  eqscut2  27865  scutun12  27869  scutbdaybnd  27874  scutbdaybnd2  27875  scutbdaylt  27877  madebdaylemlrcut  27951  cofcut1  27968  cofcutr  27972  dfn0s2  28350  shintcli  31357  shsval2i  31415  ococin  31436  chsupsn  31441  elrgspnlem4  33234  fldgensdrg  33295  fldgenssv  33296  fldgenssp  33299  insiga  34117  ldsysgenld  34140  ldgenpisyslem2  34144  mclsssvlem  35546  mclsax  35553  mclsind  35554  untint  35691  dfon2lem8  35771  dfon2lem9  35772  clsint2  36311  topmeet  36346  topjoin  36347  heibor1lem  37795  ismrcd1  42685  mzpincl  42721  mzpf  42723  mzpindd  42733  onintunirab  43215  oninfint  43224  clublem  43599  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  intsaluni  46284  intsal  46285  salgenss  46291  salgencntex  46298  intubeu  48772