Theorem intss1 4987

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 3492	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4976	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2832	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2833	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3609	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	biimtrid 242	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 4014	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1535   = wceq 1537   ∈ wcel 2108   ⊆ wss 3976  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-int 4971

This theorem is referenced by:  intminss  4998  intmin3  5000  intab  5002  int0el  5003  trintss  5302  intex  5362  intidg  5477  oneqmini  6447  sorpssint  7768  onint  7826  onssmin  7828  onnmin  7834  nnawordex  8693  cofon1  8728  cofonr  8730  dffi2  9492  inficl  9494  dffi3  9500  tcmin  9810  tc2  9811  rankr1ai  9867  rankuni2b  9922  tcrank  9953  harval2  10066  cfflb  10328  fin23lem20  10406  fin23lem38  10418  isf32lem2  10423  intwun  10804  inttsk  10843  intgru  10883  dfnn2  12306  dfuzi  12734  trclubi  15045  trclubgi  15046  trclub  15047  trclubg  15048  cotrtrclfv  15061  trclun  15063  dfrtrcl2  15111  mremre  17662  isacs1i  17715  mrelatglb  18630  cycsubg  19248  efgrelexlemb  19792  efgcpbllemb  19797  frgpuplem  19814  primefld  20828  cssmre  21734  toponmre  23122  1stcfb  23474  ptcnplem  23650  fbssfi  23866  uffix  23950  ufildom1  23955  alexsublem  24073  alexsubALTlem4  24079  tmdgsum2  24125  bcth3  25384  limciun  25949  aalioulem3  26394  sltval2  27719  sltres  27725  nocvxminlem  27840  eqscut2  27869  scutun12  27873  scutbdaybnd  27878  scutbdaybnd2  27879  scutbdaylt  27881  madebdaylemlrcut  27955  cofcut1  27972  cofcutr  27976  dfn0s2  28354  shintcli  31361  shsval2i  31419  ococin  31440  chsupsn  31445  fldgensdrg  33281  fldgenssv  33282  fldgenssp  33285  insiga  34101  ldsysgenld  34124  ldgenpisyslem2  34128  mclsssvlem  35530  mclsax  35537  mclsind  35538  untint  35674  dfon2lem8  35754  dfon2lem9  35755  clsint2  36295  topmeet  36330  topjoin  36331  heibor1lem  37769  ismrcd1  42654  mzpincl  42690  mzpf  42692  mzpindd  42702  rgspnmin  43128  onintunirab  43188  oninfint  43197  clublem  43572  dftrcl3  43682  brtrclfv2  43689  dfrtrcl3  43695  intsaluni  46250  intsal  46251  salgenss  46257  salgencntex  46264  intubeu  48656