Theorem dfss2 3407

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 3405	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3397	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2483	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2580	. . 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 279	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 642	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1699	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 260	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   A.wal 1450   = wceq 1452   e. wcel 1904   {cab 2457   i^i cin 3389   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  dfss3  3408  dfss2f  3409  ssel  3412  ssriv  3422  ssrdv  3424  sstr2  3425  eqss  3433  nss  3476  rabss2  3498  ssconb  3555  ssequn1  3595  unss  3599  ssin  3645  ssdif0  3741  difin0ss  3745  inssdif0  3746  reldisj  3812  ssundif  3842  sbcssg  3871  pwss  3957  snss  4087  pwpw0  4111  pwsnALT  4185  ssuni  4212  unissb  4221  iunss  4310  dftr2  4492  axpweq  4578  axpow2  4581  ssextss  4654  ssrel  4928  ssrel2  4930  ssrelrel  4940  reliun  4959  relop  4990  issref  5219  funimass4  5930  dfom2  6713  inf2  8146  grothpw  9269  grothprim  9277  psslinpr  9474  ltaddpr  9477  isprm2  14711  vdwmc2  15008  acsmapd  16502  dfcon2  20511  iskgen3  20641  metcld  22353  metcld2  22354  isch2  26957  pjnormssi  27902  ssiun3  28251  ssrelf  28297  bnj1361  29712  bnj978  29832  dffr5  30464  brsset  30727  sscoid  30751  relowlpssretop  31837  rp-fakeinunass  36231  rababg  36250  ss2iundf  36322  dfss6  36434  dfhe3  36441  snhesn  36453  dffrege76  36606  conss34  36865  sbcssOLD  36977  onfrALTlem2  36982  trsspwALT  37269  trsspwALT2  37270  snssiALTVD  37286  snssiALT  37287  sstrALT2VD  37293  sstrALT2  37294  sbcssgVD  37343  onfrALTlem2VD  37349  sspwimp  37378  sspwimpVD  37379  sspwimpcf  37380  sspwimpcfVD  37381  sspwimpALT  37385  unisnALT  37386  iunssf  37500  icccncfext  37862