Theorem ssalel 3215

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
ssalel	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem ssalel

Step	Hyp	Ref	Expression
1		dfss 3214	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3206	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2242	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2340	. . 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 206	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 389	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1518	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 187	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1395   = wceq 1397   e. wcel 2202   {cab 2217   i^i cin 3199   C_ wss 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  dfss3  3216  dfss2f  3218  ssel  3221  ssriv  3231  ssrdv  3233  sstr2  3234  eqss  3242  nssr  3287  rabss2  3310  ssconb  3340  ssequn1  3377  unss  3381  ssin  3429  ssddif  3441  reldisj  3546  ssdif0im  3559  inssdif0im  3562  ssundifim  3578  sbcssg  3603  pwss  3668  snssOLD  3799  snssb  3806  snsssn  3844  ssuni  3915  unissb  3923  intss  3949  iunss  4011  dftr2  4189  axpweq  4261  axpow2  4266  ssextss  4312  ordunisuc2r  4612  setind  4637  zfregfr  4672  tfi  4680  ssrel  4814  ssrel2  4816  ssrelrel  4826  reliun  4848  relop  4880  issref  5119  funimass4  5696  isprm2  12694  bj-inf2vnlem3  16593  bj-inf2vnlem4  16594