Theorem dfss2 3478

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 3476	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3468	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2461	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2567	. . 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 1627	. 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 1381   = wceq 1383   e. wcel 1804   {cab 2428   i^i cin 3460   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  dfss3  3479  dfss2f  3480  ssel  3483  ssriv  3493  ssrdv  3495  sstr2  3496  eqss  3504  nss  3547  rabss2  3568  ssconb  3622  ssequn1  3659  unss  3663  ssin  3705  reldisj  3856  ssdif0  3871  difin0ss  3880  inssdif0  3881  ssundif  3897  sbcssg  3925  pwss  4012  snss  4139  pwpw0  4163  pwsnALT  4229  ssuni  4256  unissb  4266  intssOLD  4293  iunss  4356  dftr2  4532  axpweq  4614  axpow2  4617  ssextss  4691  ssrel  5081  ssrel2  5083  ssrelrel  5093  reliun  5113  relop  5143  issref  5370  funimass4  5909  dfom2  6687  inf2  8043  grothpw  9207  grothprim  9215  psslinpr  9412  ltaddpr  9415  isprm2  14207  vdwmc2  14479  acsmapd  15787  bwthOLD  19889  dfcon2  19898  iskgen3  20028  metcld  21722  metcld2  21723  isch2  26119  pjnormssi  27065  ssiun3  27404  ssrelf  27444  dffr5  29158  brsset  29515  sscoid  29539  conss34  31305  icccncfext  31644  sbcssOLD  33181  onfrALTlem2  33186  trsspwALT  33484  trsspwALT2  33485  snssiALTVD  33495  snssiALT  33496  sstrALT2VD  33502  sstrALT2  33503  sbcssgVD  33551  onfrALTlem2VD  33557  sspwimp  33586  sspwimpVD  33587  sspwimpcf  33588  sspwimpcfVD  33589  sspwimpALT  33593  unisnALT  33594  bnj1361  33755  bnj978  33875  rp-fakeinunass  37578  dfhe3  37621  snhesn  37631