Theorem dfss2 3430

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 3428	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3420	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2420	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2526	. . 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 628	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1661	. 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 367   A.wal 1403   = wceq 1405   e. wcel 1842   {cab 2387   i^i cin 3412   C_ wss 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3420  df-ss 3427

This theorem is referenced by:  dfss3  3431  dfss2f  3432  ssel  3435  ssriv  3445  ssrdv  3447  sstr2  3448  eqss  3456  nss  3499  rabss2  3521  ssconb  3575  ssequn1  3612  unss  3616  ssin  3660  reldisj  3812  ssdif0  3827  difin0ss  3837  inssdif0  3838  ssundif  3854  sbcssg  3883  pwss  3969  snss  4095  pwpw0  4119  pwsnALT  4185  ssuni  4212  unissb  4221  intssOLD  4248  iunss  4311  dftr2  4490  axpweq  4570  axpow2  4573  ssextss  4644  ssrel  4911  ssrel2  4913  ssrelrel  4923  reliun  4942  relop  4973  issref  5200  funimass4  5899  dfom2  6684  inf2  8072  grothpw  9233  grothprim  9241  psslinpr  9438  ltaddpr  9441  isprm2  14432  vdwmc2  14704  acsmapd  16130  dfcon2  20210  iskgen3  20340  metcld  22034  metcld2  22035  isch2  26541  pjnormssi  27486  ssiun3  27841  ssrelf  27889  bnj1361  29201  bnj978  29321  dffr5  29953  brsset  30214  sscoid  30238  rp-fakeinunass  35587  ss2iundf  35618  dfss6  35728  dfhe3  35735  snhesn  35747  dffrege76  35900  conss34  36179  sbcssOLD  36317  onfrALTlem2  36322  trsspwALT  36620  trsspwALT2  36621  snssiALTVD  36637  snssiALT  36638  sstrALT2VD  36644  sstrALT2  36645  sbcssgVD  36694  onfrALTlem2VD  36700  sspwimp  36729  sspwimpVD  36730  sspwimpcf  36731  sspwimpcfVD  36732  sspwimpALT  36736  unisnALT  36737  icccncfext  37039