Theorem intss1 4492

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 3203	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4481	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2689	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2690	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 334	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3293	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 232	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3609	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1481   = wceq 1483   ∈ wcel 1990   ⊆ wss 3574  ∩ cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-int 4476

This theorem is referenced by:  intminss  4503  intmin3  4505  intab  4507  int0el  4508  trintss  4769  intex  4820  oneqmini  5776  sorpssint  6947  onint  6995  onssmin  6997  onnmin  7003  nnawordex  7717  dffi2  8329  inficl  8331  dffi3  8337  tcmin  8617  tc2  8618  rankr1ai  8661  rankuni2b  8716  tcrank  8747  harval2  8823  cfflb  9081  fin23lem20  9159  fin23lem38  9171  isf32lem2  9176  intwun  9557  inttsk  9596  intgru  9636  dfnn2  11033  dfuzi  11468  trclubi  13735  trclubiOLD  13736  trclubgi  13737  trclubgiOLD  13738  trclub  13739  trclubg  13740  cotrtrclfv  13753  trclun  13755  dfrtrcl2  13802  mremre  16264  isacs1i  16318  mrelatglb  17184  cycsubg  17622  efgrelexlemb  18163  efgcpbllemb  18168  frgpuplem  18185  cssmre  20037  toponmre  20897  1stcfb  21248  ptcnplem  21424  fbssfi  21641  uffix  21725  ufildom1  21730  alexsublem  21848  alexsubALTlem4  21854  tmdgsum2  21900  bcth3  23128  limciun  23658  aalioulem3  24089  shintcli  28188  shsval2i  28246  ococin  28267  chsupsn  28272  insiga  30200  ldsysgenld  30223  ldgenpisyslem2  30227  mclsssvlem  31459  mclsax  31466  mclsind  31467  untint  31589  dfon2lem8  31695  dfon2lem9  31696  sltval2  31809  sltres  31815  nocvxminlem  31893  scutun12  31917  scutbdaybnd  31921  scutbdaylt  31922  clsint2  32324  topmeet  32359  topjoin  32360  heibor1lem  33608  ismrcd1  37261  mzpincl  37297  mzpf  37299  mzpindd  37309  rgspnmin  37741  clublem  37917  dftrcl3  38012  brtrclfv2  38019  dfrtrcl3  38025  intsaluni  40547  intsal  40548  salgenss  40554  salgencntex  40561