Theorem intss1 4894

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 3500	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4885	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2903	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2904	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3598	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 244	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3976	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1534   = wceq 1536   ∈ wcel 2113   ⊆ wss 3939  ∩ cint 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-in 3946  df-ss 3955  df-int 4880

This theorem is referenced by:  intminss  4905  intmin3  4907  intab  4909  int0el  4910  trintss  5192  intex  5243  oneqmini  6245  sorpssint  7462  onint  7513  onssmin  7515  onnmin  7521  nnawordex  8266  dffi2  8890  inficl  8892  dffi3  8898  tcmin  9186  tc2  9187  rankr1ai  9230  rankuni2b  9285  tcrank  9316  harval2  9429  cfflb  9684  fin23lem20  9762  fin23lem38  9774  isf32lem2  9779  intwun  10160  inttsk  10199  intgru  10239  dfnn2  11654  dfuzi  12076  trclubi  14359  trclubgi  14360  trclub  14361  trclubg  14362  cotrtrclfv  14375  trclun  14377  dfrtrcl2  14424  mremre  16878  isacs1i  16931  mrelatglb  17797  cycsubg  18354  efgrelexlemb  18879  efgcpbllemb  18884  frgpuplem  18901  primefld  19587  cssmre  20840  toponmre  21704  1stcfb  22056  ptcnplem  22232  fbssfi  22448  uffix  22532  ufildom1  22537  alexsublem  22655  alexsubALTlem4  22661  tmdgsum2  22707  bcth3  23937  limciun  24495  aalioulem3  24926  shintcli  29109  shsval2i  29167  ococin  29188  chsupsn  29193  insiga  31400  ldsysgenld  31423  ldgenpisyslem2  31427  mclsssvlem  32813  mclsax  32820  mclsind  32821  untint  32942  dfon2lem8  33039  dfon2lem9  33040  sltval2  33167  sltres  33173  nocvxminlem  33251  scutun12  33275  scutbdaybnd  33279  scutbdaylt  33280  clsint2  33681  topmeet  33716  topjoin  33717  heibor1lem  35091  ismrcd1  39301  mzpincl  39337  mzpf  39339  mzpindd  39349  rgspnmin  39777  clublem  39976  dftrcl3  40071  brtrclfv2  40078  dfrtrcl3  40084  intsaluni  42619  intsal  42620  salgenss  42626  salgencntex  42633