Theorem dfss2 3445

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 3443	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3435	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2469	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2575	. . 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 1611	. 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 1368   = wceq 1370   e. wcel 1758   {cab 2436   i^i cin 3427   C_ wss 3428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3435  df-ss 3442

This theorem is referenced by:  dfss3  3446  dfss2f  3447  ssel  3450  ssriv  3460  ssrdv  3462  sstr2  3463  eqss  3471  nss  3514  rabss2  3535  ssconb  3589  ssequn1  3626  unss  3630  ssin  3672  reldisj  3822  ssdif0  3837  difin0ss  3845  inssdif0  3846  ssundif  3862  sbcssg  3890  pwss  3975  snss  4099  pwpw0  4121  pwsnALT  4186  ssuni  4213  unissb  4223  intss  4249  iunss  4311  dftr2  4487  axpweq  4569  axpow2  4572  ssextss  4646  ssrel  5028  ssrel2  5030  ssrelrel  5040  reliun  5060  relop  5090  issref  5311  funimass4  5843  dfom2  6580  inf2  7932  grothpw  9096  grothprim  9104  psslinpr  9303  ltaddpr  9306  isprm2  13875  vdwmc2  14144  acsmapd  15452  bwthOLD  19132  dfcon2  19141  iskgen3  19240  metcld  20934  metcld2  20935  isch2  24763  pjnormssi  25709  ssiun3  26045  ssrelf  26081  dffr5  27699  brsset  28056  sscoid  28080  conss34  29838  clwwlkssclwwlkn  30594  sbcssOLD  31551  onfrALTlem2  31556  trsspwALT  31854  trsspwALT2  31855  snssiALTVD  31865  snssiALT  31866  sstrALT2VD  31872  sstrALT2  31873  sbcssgVD  31921  onfrALTlem2VD  31927  sspwimp  31956  sspwimpVD  31957  sspwimpcf  31958  sspwimpcfVD  31959  sspwimpALT  31963  unisnALT  31964  bnj1361  32124  bnj978  32244