Theorem ssalel 3229

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 3228	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3220	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2245	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2343	. . 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 1519	. 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 1396   = wceq 1398   e. wcel 2205   {cab 2220   i^i cin 3213   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  dfss3  3230  dfssf  3232  dfss2f  3233  ssel  3236  ssriv  3246  ssrdv  3248  sstr2  3249  eqss  3257  nssr  3302  rabss2  3325  ssconb  3356  ssequn1  3393  unss  3397  ssin  3447  ssddif  3459  reldisj  3564  ssdif0im  3577  inssdif0im  3580  ssundifim  3597  sbcssg  3622  pwss  3693  snssOLD  3824  snssb  3832  snsssn  3870  ssuni  3941  unissb  3949  intss  3975  iunss  4037  dftr2  4215  axpweq  4289  axpow2  4294  ssextss  4341  ordunisuc2r  4641  setind  4666  zfregfr  4701  tfi  4709  ssrel  4843  ssrel2  4845  ssrelrel  4855  reliun  4878  relop  4910  issref  5150  funimass4  5732  isprm2  12839  bj-inf2vnlem3  16854  bj-inf2vnlem4  16855