Theorem ssintub 4919

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 4917	. 2 ⊢ (𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ ∀𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}𝐴 ⊆ 𝑦)
2		sseq2 3958	. . . 4 ⊢ (𝑥 = 𝑦 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦))
3	2	elrab 3644	. . 3 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} ↔ (𝑦 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑦))
4	3	simprbi 496	. 2 ⊢ (𝑦 ∈ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥} → 𝐴 ⊆ 𝑦)
5	1, 4	mprgbir 3056	1 ⊢ 𝐴 ⊆ ∩ {𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥}

Syntax hints:   ∈ wcel 2113  {crab 3397   ⊆ wss 3899  ∩ cint 4900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-11 2162  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rab 3398  df-v 3440  df-ss 3916  df-int 4901

This theorem is referenced by:  intmin  4921  cofon2  8599  naddunif  8619  wuncid  10652  mrcssid  17538  rgspnssid  20545  lspssid  20934  lbsextlem3  21113  aspssid  21831  sscls  22998  filufint  23862  spanss2  31369  shsval2i  31411  ococin  31432  chsupsn  31437  fldgenssid  33344  sssigagen  34251  dynkin  34273  igenss  38202  pclssidN  40094  dochocss  41565  intubeu  49171