Theorem dfss2 3297

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 3295	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3287	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2414	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2509	. . 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 263	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 612	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1572	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 244	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   A.wal 1546   = wceq 1649   e. wcel 1721   {cab 2390   i^i cin 3279   C_ wss 3280

This theorem is referenced by:  dfss3  3298  dfss2f  3299  ssel  3302  ssriv  3312  ssrdv  3314  sstr2  3315  eqss  3323  nss  3366  rabss2  3386  ssconb  3440  ssequn1  3477  unss  3481  ssin  3523  reldisj  3631  ssdif0  3646  difin0ss  3654  inssdif0  3655  ssundif  3671  sbcss  3698  pwss  3773  snss  3886  pwpw0  3906  pwsnALT  3970  ssuni  3997  unissb  4005  intss  4031  iunss  4092  dftr2  4264  axpweq  4336  axpow2  4339  ssextss  4377  dfom2  4806  ssrel  4923  ssrel2  4925  ssrelrel  4935  reliun  4954  relop  4982  issref  5206  funimass4  5736  inf2  7534  grothpw  8657  grothprim  8665  psslinpr  8864  ltaddpr  8867  isprm2  13042  vdwmc2  13302  acsmapd  14559  dfcon2  17435  iskgen3  17534  metcld  19211  metcld2  19212  isch2  22679  pjnormssi  23624  ssiun3  23962  dffr5  25324  brsset  25643  conss34  27512  sbcssOLD  28338  onfrALTlem2  28343  trsspwALT  28640  trsspwALT2  28641  snssiALTVD  28648  snssiALT  28649  sstrALT2VD  28655  sstrALT2  28656  sbcssVD  28704  onfrALTlem2VD  28710  sspwimp  28739  sspwimpVD  28740  sspwimpcf  28741  sspwimpcfVD  28742  sspwimpALT  28746  unisnALT  28747  bnj1361  28906  bnj978  29026

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294