Theorem ssint 4921

Description: Subclass of a class intersection. Theorem 5.11(viii) of [Monk1] p. 52 and its converse. (Contributed by NM, 14-Oct-1999.)

Assertion

Ref	Expression
ssint	⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ssint

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss3 3925	. 2 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵)
2		vex 3457	. . . 4 ⊢ 𝑦 ∈ V
3	2	elint2 4911	. . 3 ⊢ (𝑦 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
4	3	ralbii 3107	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
5		ralcom 3289	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
6		dfss3 3925	. . . 4 ⊢ (𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
7	6	ralbii 3107	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
8	5, 7	bitr4i 280	. 2 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
9	1, 4, 8	3bitri 299	1 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)

Syntax hints:   ↔ wb 208   ∈ wcel 2141  ∀wral 3075   ⊆ wss 3904  ∩ cint 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-11 2190  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-v 3455  df-ss 3921  df-int 4905

This theorem is referenced by:  ssintab  4922  ssintub  4923  iinpw  5062  oneqmini  6395  fint  6739  fnssintima  7342  sorpssint  7712  iscard2  9931  coftr  10227  isf32lem2  10308  inttsk  10729  dfrtrcl2  15072  isacs1i  17672  mrelatglb  18575  fbfinnfr  23881  fclscmp  24070  noextenddif  27709  eqcuts2  27856  cutsun12  27860  oniso  28341  bdayn0p1  28439  ssdifidllem  33604  ssmxidllem  33622  fneint  36672  topmeet  36688  igenval2  38529  ismrcd1  43243  onintunirab  43768  dftrcl3  44260  dfrtrcl3  44273  sssalgen  46873  issalgend  46876  intubeu  49569  ipoglblem  49574