Theorem dfss2 2055

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
dfss2	⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))

Distinct variable groups:   x,A   x,B

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 2051	. . 3 ⊢ (A ⊆ B ↔ A = (A ∩ B))
2		df-in 2048	. . . 4 ⊢ (A ∩ B) = {x∣(x ∈ A ⋀ x ∈ B)}
3	2	eqeq2i 1483	. . 3 ⊢ (A = (A ∩ B) ↔ A = {x∣(x ∈ A ⋀ x ∈ B)})
4		abeq2 1566	. . 3 ⊢ (A = {x∣(x ∈ A ⋀ x ∈ B)} ↔ ∀x(x ∈ A ↔ (x ∈ A ⋀ x ∈ B)))
5	1, 3, 4	3bitr 177	. 2 ⊢ (A ⊆ B ↔ ∀x(x ∈ A ↔ (x ∈ A ⋀ x ∈ B)))
6		pm4.71 634	. . 3 ⊢ ((x ∈ A → x ∈ B) ↔ (x ∈ A ↔ (x ∈ A ⋀ x ∈ B)))
7	6	albii 998	. 2 ⊢ (∀x(x ∈ A → x ∈ B) ↔ ∀x(x ∈ A ↔ (x ∈ A ⋀ x ∈ B)))
8	5, 7	bitr4 176	1 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  {cab 1462   ∩ cin 2043   ⊆ wss 2044

This theorem is referenced by:  dfss3 2056  dfss2f 2057  ssel 2060  ssriv 2066  ssrdv 2067  sstr2 2068  eqss 2074  nss 2110  rabss2 2126  ssconb 2167  unss1 2196  ssequn1 2197  unss 2201  ssrin 2231  reldisj 2310  ssdif0 2324  difin0ss 2329  inssdif0 2330  ssundif 2341  snss 2458  pwpw0 2466  prsspw 2477  ssuni 2518  unissb 2524  intss 2550  iunss 2587  ssiun 2588  ssiin 2595  iinss 2596  dftr2 2678  pwex 2741  ssextss 2758  dfom2 3129  ssrel 3243  reluni 3261  relop 3271  dmcosseq 3361  funimass4 3758  inf2 4591  setind2 4632  psslinpr 5118  prlem934 5122  ltaddpr 5123  tgss3t 7598  metcld 7929  grothprim 8738  pjnormss 10052  uninqs 10400  hst1 10533

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-in 2048  df-ss 2050

Copyright terms: Public domain