Theorem intss1 4524

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 3234	. . . 4 ⊢ 𝑥 ∈ V
2	1	elint 4513	. . 3 ⊢ (𝑥 ∈ ∩ 𝐵 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦))
3		eleq1 2718	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
4		eleq2 2719	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴))
5	3, 4	imbi12d 333	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) ↔ (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
6	5	spcgv 3324	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → (𝐴 ∈ 𝐵 → 𝑥 ∈ 𝐴)))
7	6	pm2.43a 54	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑦(𝑦 ∈ 𝐵 → 𝑥 ∈ 𝑦) → 𝑥 ∈ 𝐴))
8	2, 7	syl5bi 232	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝑥 ∈ ∩ 𝐵 → 𝑥 ∈ 𝐴))
9	8	ssrdv 3642	1 ⊢ (𝐴 ∈ 𝐵 → ∩ 𝐵 ⊆ 𝐴)

Syntax hints:   → wi 4  ∀wal 1521   = wceq 1523   ∈ wcel 2030   ⊆ wss 3607  ∩ cint 4507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621  df-int 4508

This theorem is referenced by:  intminss  4535  intmin3  4537  intab  4539  int0el  4540  trintss  4802  intex  4850  oneqmini  5814  sorpssint  6989  onint  7037  onssmin  7039  onnmin  7045  nnawordex  7762  dffi2  8370  inficl  8372  dffi3  8378  tcmin  8655  tc2  8656  rankr1ai  8699  rankuni2b  8754  tcrank  8785  harval2  8861  cfflb  9119  fin23lem20  9197  fin23lem38  9209  isf32lem2  9214  intwun  9595  inttsk  9634  intgru  9674  dfnn2  11071  dfuzi  11506  trclubi  13781  trclubgi  13782  trclub  13783  trclubg  13784  cotrtrclfv  13797  trclun  13799  dfrtrcl2  13846  mremre  16311  isacs1i  16365  mrelatglb  17231  cycsubg  17669  efgrelexlemb  18209  efgcpbllemb  18214  frgpuplem  18231  cssmre  20085  toponmre  20945  1stcfb  21296  ptcnplem  21472  fbssfi  21688  uffix  21772  ufildom1  21777  alexsublem  21895  alexsubALTlem4  21901  tmdgsum2  21947  bcth3  23174  limciun  23703  aalioulem3  24134  shintcli  28316  shsval2i  28374  ococin  28395  chsupsn  28400  insiga  30328  ldsysgenld  30351  ldgenpisyslem2  30355  mclsssvlem  31585  mclsax  31592  mclsind  31593  untint  31715  dfon2lem8  31819  dfon2lem9  31820  sltval2  31934  sltres  31940  nocvxminlem  32018  scutun12  32042  scutbdaybnd  32046  scutbdaylt  32047  clsint2  32449  topmeet  32484  topjoin  32485  heibor1lem  33738  ismrcd1  37578  mzpincl  37614  mzpf  37616  mzpindd  37626  rgspnmin  38058  clublem  38234  dftrcl3  38329  brtrclfv2  38336  dfrtrcl3  38342  intsaluni  40865  intsal  40866  salgenss  40872  salgencntex  40879