Theorem dfss2 3450

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 3448	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3440	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2438	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2544	. . 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 274	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 634	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1687	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 255	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   e. wcel 1867   {cab 2405   i^i cin 3432   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447

This theorem is referenced by:  dfss3  3451  dfss2f  3452  ssel  3455  ssriv  3465  ssrdv  3467  sstr2  3468  eqss  3476  nss  3519  rabss2  3541  ssconb  3595  ssequn1  3633  unss  3637  ssin  3681  reldisj  3833  ssdif0  3848  difin0ss  3858  inssdif0  3859  ssundif  3876  sbcssg  3905  pwss  3991  snss  4118  pwpw0  4142  pwsnALT  4208  ssuni  4235  unissb  4244  intssOLD  4271  iunss  4334  dftr2  4514  axpweq  4594  axpow2  4597  ssextss  4668  ssrel  4935  ssrel2  4937  ssrelrel  4947  reliun  4966  relop  4997  issref  5225  funimass4  5924  dfom2  6700  inf2  8126  grothpw  9247  grothprim  9255  psslinpr  9452  ltaddpr  9455  isprm2  14610  vdwmc2  14907  acsmapd  16402  dfcon2  20411  iskgen3  20541  metcld  22252  metcld2  22253  isch2  26852  pjnormssi  27797  ssiun3  28153  ssrelf  28201  bnj1361  29629  bnj978  29749  dffr5  30381  brsset  30642  sscoid  30666  relowlpssretop  31702  rp-fakeinunass  36074  ss2iundf  36105  dfss6  36215  dfhe3  36222  snhesn  36234  dffrege76  36387  conss34  36647  sbcssOLD  36759  onfrALTlem2  36764  trsspwALT  37061  trsspwALT2  37062  snssiALTVD  37078  snssiALT  37079  sstrALT2VD  37085  sstrALT2  37086  sbcssgVD  37135  onfrALTlem2VD  37141  sspwimp  37170  sspwimpVD  37171  sspwimpcf  37172  sspwimpcfVD  37173  sspwimpALT  37177  unisnALT  37178  icccncfext  37552