Theorem dfss2 3488

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	|- ( 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 3486	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3478	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2480	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2586	. . 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 271	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 630	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1615	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 252	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1372   = wceq 1374   e. wcel 1762   {cab 2447   i^i cin 3470   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3478  df-ss 3485

This theorem is referenced by:  dfss3  3489  dfss2f  3490  ssel  3493  ssriv  3503  ssrdv  3505  sstr2  3506  eqss  3514  nss  3557  rabss2  3578  ssconb  3632  ssequn1  3669  unss  3673  ssin  3715  reldisj  3865  ssdif0  3880  difin0ss  3888  inssdif0  3889  ssundif  3905  sbcssg  3933  pwss  4020  snss  4146  pwpw0  4170  pwsnALT  4235  ssuni  4262  unissb  4272  intss  4298  iunss  4361  dftr2  4537  axpweq  4619  axpow2  4622  ssextss  4696  ssrel  5084  ssrel2  5086  ssrelrel  5096  reliun  5116  relop  5146  issref  5373  funimass4  5911  dfom2  6675  inf2  8031  grothpw  9195  grothprim  9203  psslinpr  9400  ltaddpr  9403  isprm2  14075  vdwmc2  14347  acsmapd  15656  bwthOLD  19672  dfcon2  19681  iskgen3  19780  metcld  21474  metcld2  21475  clwwlkssclwwlkn  24456  isch2  25805  pjnormssi  26751  ssiun3  27087  ssrelf  27127  dffr5  28747  brsset  29104  sscoid  29128  conss34  30886  fzssz  31000  icccncfext  31183  sbcssOLD  32270  onfrALTlem2  32275  trsspwALT  32573  trsspwALT2  32574  snssiALTVD  32584  snssiALT  32585  sstrALT2VD  32591  sstrALT2  32592  sbcssgVD  32640  onfrALTlem2VD  32646  sspwimp  32675  sspwimpVD  32676  sspwimpcf  32677  sspwimpcfVD  32678  sspwimpALT  32682  unisnALT  32683  bnj1361  32843  bnj978  32963