Theorem ssint 4892

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 3905	. 2 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵)
2		vex 3426	. . . 4 ⊢ 𝑦 ∈ V
3	2	elint2 4883	. . 3 ⊢ (𝑦 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
4	3	ralbii 3090	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
5		ralcom 3280	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
6		dfss3 3905	. . . 4 ⊢ (𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
7	6	ralbii 3090	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
8	5, 7	bitr4i 277	. 2 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
9	1, 4, 8	3bitri 296	1 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)

Syntax hints:   ↔ wb 205   ∈ wcel 2108  ∀wral 3063   ⊆ wss 3883  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-int 4877

This theorem is referenced by:  ssintab  4893  ssintub  4894  iinpw  5031  oneqmini  6302  fint  6637  sorpssint  7564  iscard2  9665  coftr  9960  isf32lem2  10041  inttsk  10461  dfrtrcl2  14701  isacs1i  17283  mrelatglb  18193  fbfinnfr  22900  fclscmp  23089  ssmxidllem  31543  fnssintima  33578  noextenddif  33798  eqscut2  33927  scutun12  33931  fneint  34464  topmeet  34480  igenval2  36151  ismrcd1  40436  dftrcl3  41217  dfrtrcl3  41230  sssalgen  43764  issalgend  43767  intubeu  46158  ipoglblem  46163