Theorem ssint 4884

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 3955	. 2 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵)
2		vex 3497	. . . 4 ⊢ 𝑦 ∈ V
3	2	elint2 4875	. . 3 ⊢ (𝑦 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
4	3	ralbii 3165	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝑦 ∈ ∩ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥)
5		ralcom 3354	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
6		dfss3 3955	. . . 4 ⊢ (𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
7	6	ralbii 3165	. . 3 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥 ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ∈ 𝑥)
8	5, 7	bitr4i 280	. 2 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)
9	1, 4, 8	3bitri 299	1 ⊢ (𝐴 ⊆ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ⊆ 𝑥)

Syntax hints:   ↔ wb 208   ∈ wcel 2110  ∀wral 3138   ⊆ wss 3935  ∩ cint 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3496  df-in 3942  df-ss 3951  df-int 4869

This theorem is referenced by:  ssintab  4885  ssintub  4886  iinpw  5020  oneqmini  6236  fint  6552  sorpssint  7453  iscard2  9399  coftr  9689  isf32lem2  9770  inttsk  10190  dfrtrcl2  14415  isacs1i  16922  mrelatglb  17788  fbfinnfr  22443  fclscmp  22632  ssmxidllem  30973  noextenddif  33170  scutun12  33266  fneint  33691  topmeet  33707  igenval2  35338  ismrcd1  39288  dftrcl3  40058  dfrtrcl3  40071  sssalgen  42612  issalgend  42615