Theorem intss1 4968

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 3479	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4957	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2823	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3587	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 241	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3989	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1540   = wceq 1542   ∈ wcel 2107   ⊆ wss 3949  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-int 4952

This theorem is referenced by:  intminss  4979  intmin3  4981  intab  4983  int0el  4984  trintss  5285  intex  5338  intidg  5458  oneqmini  6417  sorpssint  7723  onint  7778  onssmin  7780  onnmin  7786  nnawordex  8637  cofon1  8671  cofonr  8673  dffi2  9418  inficl  9420  dffi3  9426  tcmin  9736  tc2  9737  rankr1ai  9793  rankuni2b  9848  tcrank  9879  harval2  9992  cfflb  10254  fin23lem20  10332  fin23lem38  10344  isf32lem2  10349  intwun  10730  inttsk  10769  intgru  10809  dfnn2  12225  dfuzi  12653  trclubi  14943  trclubgi  14944  trclub  14945  trclubg  14946  cotrtrclfv  14959  trclun  14961  dfrtrcl2  15009  mremre  17548  isacs1i  17601  mrelatglb  18513  cycsubg  19085  efgrelexlemb  19618  efgcpbllemb  19623  frgpuplem  19640  primefld  20421  cssmre  21246  toponmre  22597  1stcfb  22949  ptcnplem  23125  fbssfi  23341  uffix  23425  ufildom1  23430  alexsublem  23548  alexsubALTlem4  23554  tmdgsum2  23600  bcth3  24848  limciun  25411  aalioulem3  25847  sltval2  27159  sltres  27165  nocvxminlem  27279  eqscut2  27307  scutun12  27311  scutbdaybnd  27316  scutbdaybnd2  27317  scutbdaylt  27319  madebdaylemlrcut  27393  cofcut1  27407  cofcutr  27411  shintcli  30582  shsval2i  30640  ococin  30661  chsupsn  30666  fldgensdrg  32404  fldgenssv  32405  fldgenssp  32408  insiga  33135  ldsysgenld  33158  ldgenpisyslem2  33162  mclsssvlem  34553  mclsax  34560  mclsind  34561  untint  34681  dfon2lem8  34762  dfon2lem9  34763  clsint2  35214  topmeet  35249  topjoin  35250  heibor1lem  36677  ismrcd1  41436  mzpincl  41472  mzpf  41474  mzpindd  41484  rgspnmin  41913  onintunirab  41976  oninfint  41985  clublem  42361  dftrcl3  42471  brtrclfv2  42478  dfrtrcl3  42484  intsaluni  45045  intsal  45046  salgenss  45052  salgencntex  45059  intubeu  47609