Theorem dfss2 2841

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

Assertion

Ref	Expression
dfss2	|- (A C_ B <-> A.x(x e. A -> x e. B))

Distinct variable groups:   x,A   x,B

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 2837	. . 3 |- (A C_ B <-> A = (A i^i B))
2		df-in 2834	. . . 4 |- (A i^i B) = {x | (x e. A /\ x e. B)}
3	2	eqeq2i 2151	. . 3 |- (A = (A i^i B) <-> A = {x | (x e. A /\ x e. B)})
4		abeq2 2248	. . 3 |- (A = {x | (x e. A /\ x e. B)} <-> A.x(x e. A <-> (x e. A /\ x e. B)))
5	1, 3, 4	3bitri 289	. 2 |- (A C_ B <-> A.x(x e. A <-> (x e. A /\ x e. B)))
6		pm4.71 957	. . 3 |- ((x e. A -> x e. B) <-> (x e. A <-> (x e. A /\ x e. B)))
7	6	albii 1635	. 2 |- (A.x(x e. A -> x e. B) <-> A.x(x e. A <-> (x e. A /\ x e. B)))
8	5, 7	bitr4i 283	1 |- (A C_ B <-> A.x(x e. A -> x e. B))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  {cab 2128   i^i cin 2826   C_ wss 2827

This theorem is referenced by:  dfss3 2842  dfss2f 2843  ssel 2846  ssriv 2852  ssrdv 2853  sstr2 2854  eqss 2860  nss 2898  rabss2 2915  ssconb 2957  ssequn1 2989  unss 2993  ssin 3028  reldisj 3121  ssdif0 3135  difin0ss 3140  inssdif0 3141  ssundif 3154  sbsslem 3178  pwss 3237  snss 3317  pwpw0 3326  pwsnALT 3362  ssuni 3388  unissb 3394  intss 3421  iunss 3467  ssiinf 3475  dftr2 3581  axpweq 3648  axpow2 3651  ssextss 3671  dfom2 4087  ssrel 4208  ssrelrel 4215  reliun 4231  relop 4242  funimass4 4808  inf2 5946  setind2 5996  sbcss 6075  onfrALTlem2 6080  psslinpr 6653  prlem934 6657  ltaddpr 6658  suprzcl 7997  gcdcllem3 9314  isprm2 9369  tgss3 9759  metcld 10111  gafo 10320  grothpw 11005  grothprim 11012  usinuniop 11179  pjnormssi 12571  bnj215 13280  bnj1361 13857  bnj849 14089  bnj978 14126  bnj1031 14154  bnj1067 14170  dffr5 14463  fundmpss 14467  brsset 14754  limitssson 14772  uninqs 15048  domfldrefc 15071  ranfldrefc 15072  ref4w 15080  ssiingOLD 15196  tolat 15370  hst1 15728  bwt2 15738  cntrsetlem 15791  tclinf 16051  fnctartar 16094  fnctartar2 16095  neibastop2lem3 16345  limfilcf 16411  fcluscf 16436  conss34 17243  conss1 17245  trsspwALT 17474  trsspwALT2 17475  snssiALTVD 17484  snssiALT 17485  sstrALT2VD 17492  sstrALT2 17493  sbcssVD 17541  onfrALTlem2VD 17547

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-10 1596  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-in 2834  df-ss 2836

Copyright terms: Public domain