Theorem ssintub 4897

Description: Subclass of the least upper bound. (Contributed by NM, 8-Aug-2000.)

Assertion

Ref	Expression
ssintub	⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssintub

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssint 4895	. 2 ⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}𝐴 ⊆ 𝑦)
2		sseq2 3947	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦))
3	2	elrab 3624	. . 3 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ (𝑦 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑦))
4	3	simprbi 497	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝐴 ⊆ 𝑦)
5	1, 4	mprgbir 3079	1 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}

Syntax hints:   ∈ wcel 2106  {crab 3068   ⊆ wss 3887  ∩ cint 4879

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-int 4880

This theorem is referenced by:  intmin  4899  wuncid  10499  mrcssid  17326  lspssid  20247  lbsextlem3  20422  aspssid  21082  sscls  22207  filufint  23071  spanss2  29707  shsval2i  29749  ococin  29770  chsupsn  29775  sssigagen  32113  dynkin  32135  igenss  36220  pclssidN  37909  dochocss  39380  rgspnssid  40995  intubeu  46270