Theorem dfss2 3420

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 3418	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3410	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2462	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2559	. . 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 275	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 635	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1690	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 256	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   A.wal 1441   = wceq 1443   e. wcel 1886   {cab 2436   i^i cin 3402   C_ wss 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3410  df-ss 3417

This theorem is referenced by:  dfss3  3421  dfss2f  3422  ssel  3425  ssriv  3435  ssrdv  3437  sstr2  3438  eqss  3446  nss  3489  rabss2  3511  ssconb  3565  ssequn1  3603  unss  3607  ssin  3653  reldisj  3807  ssdif0  3822  difin0ss  3832  inssdif0  3833  ssundif  3850  sbcssg  3879  pwss  3965  snss  4095  pwpw0  4119  pwsnALT  4192  ssuni  4219  unissb  4228  intssOLD  4255  iunss  4318  dftr2  4498  axpweq  4579  axpow2  4582  ssextss  4653  ssrel  4922  ssrel2  4924  ssrelrel  4934  reliun  4953  relop  4984  issref  5212  funimass4  5914  dfom2  6691  inf2  8125  grothpw  9248  grothprim  9256  psslinpr  9453  ltaddpr  9456  isprm2  14625  vdwmc2  14922  acsmapd  16417  dfcon2  20427  iskgen3  20557  metcld  22268  metcld2  22269  isch2  26869  pjnormssi  27814  ssiun3  28166  ssrelf  28214  bnj1361  29633  bnj978  29753  dffr5  30386  brsset  30649  sscoid  30673  relowlpssretop  31760  rp-fakeinunass  36154  rababg  36173  ss2iundf  36245  dfss6  36357  dfhe3  36364  snhesn  36376  dffrege76  36529  conss34  36789  sbcssOLD  36901  onfrALTlem2  36906  trsspwALT  37200  trsspwALT2  37201  snssiALTVD  37217  snssiALT  37218  sstrALT2VD  37224  sstrALT2  37225  sbcssgVD  37274  onfrALTlem2VD  37280  sspwimp  37309  sspwimpVD  37310  sspwimpcf  37311  sspwimpcfVD  37312  sspwimpALT  37316  unisnALT  37317  icccncfext  37759