Theorem ssint 4928

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 3935	. 2 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵)
2		vex 3451	. . . 4 ⊢ 𝑦 ∈ V
3	2	elint2 4917	. . 3 ⊢ (𝑦 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
4	3	ralbii 3075	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
5		ralcom 3265	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
6		dfss3 3935	. . . 4 ⊢ (𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
7	6	ralbii 3075	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
8	5, 7	bitr4i 278	. 2 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
9	1, 4, 8	3bitri 297	1 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3914  ∩ cint 4910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-ss 3931  df-int 4911

This theorem is referenced by:  ssintab  4929  ssintub  4930  iinpw  5070  oneqmini  6385  fint  6739  fnssintima  7337  sorpssint  7709  iscard2  9929  coftr  10226  isf32lem2  10307  inttsk  10727  dfrtrcl2  15028  isacs1i  17618  mrelatglb  18519  fbfinnfr  23728  fclscmp  23917  noextenddif  27580  eqscut2  27718  scutun12  27722  onsiso  28169  bdayn0p1  28258  ssdifidllem  33427  ssmxidllem  33444  fneint  36336  topmeet  36352  igenval2  38060  ismrcd1  42686  onintunirab  43216  dftrcl3  43709  dfrtrcl3  43722  sssalgen  46333  issalgend  46336  intubeu  48972  ipoglblem  48977