Theorem ssint 4907

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3890  ∩ cint 4890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-11 2163  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3432  df-ss 3907  df-int 4891

This theorem is referenced by:  ssintab  4908  ssintub  4909  iinpw  5049  oneqmini  6370  fint  6713  fnssintima  7310  sorpssint  7680  iscard2  9891  coftr  10186  isf32lem2  10267  inttsk  10688  dfrtrcl2  15015  isacs1i  17614  mrelatglb  18517  fbfinnfr  23816  fclscmp  24005  noextenddif  27646  eqcuts2  27792  cutsun12  27796  oniso  28277  bdayn0p1  28375  ssdifidllem  33531  ssmxidllem  33548  fneint  36546  topmeet  36562  igenval2  38401  ismrcd1  43144  onintunirab  43673  dftrcl3  44165  dfrtrcl3  44178  sssalgen  46781  issalgend  46784  intubeu  49471  ipoglblem  49476