Theorem dfss2 3091

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
dfss2	⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 3090	. . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 = (𝐴 ∩ 𝐵))
2		df-in 3082	. . . 4 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3	2	eqeq2i 2151	. . 3 ⊢ (𝐴 = (𝐴 ∩ 𝐵) ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)})
4		abeq2 2249	. . 3 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5	1, 3, 4	3bitri 205	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
6		pm4.71 387	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
7	6	albii 1447	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
8	5, 7	bitr4i 186	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330   = wceq 1332   ∈ wcel 1481  {cab 2126   ∩ cin 3075   ⊆ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  dfss3  3092  dfss2f  3093  ssel  3096  ssriv  3106  ssrdv  3108  sstr2  3109  eqss  3117  nssr  3162  rabss2  3185  ssconb  3214  ssequn1  3251  unss  3255  ssin  3303  ssddif  3315  reldisj  3419  ssdif0im  3432  inssdif0im  3435  ssundifim  3451  sbcssg  3477  pwss  3531  snss  3657  snsssn  3696  ssuni  3766  unissb  3774  intss  3800  iunss  3862  dftr2  4036  axpweq  4103  axpow2  4108  ssextss  4150  ordunisuc2r  4438  setind  4462  zfregfr  4496  tfi  4504  ssrel  4635  ssrel2  4637  ssrelrel  4647  reliun  4668  relop  4697  issref  4929  funimass4  5480  isprm2  11834  bj-inf2vnlem3  13341  bj-inf2vnlem4  13342