Theorem ssalel 3216

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 3215	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3207	. . . 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 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 2202   {cab 2217   i^i cin 3200   C_ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  dfss3  3217  dfss2f  3219  ssel  3222  ssriv  3232  ssrdv  3234  sstr2  3235  eqss  3243  nssr  3288  rabss2  3311  ssconb  3342  ssequn1  3379  unss  3383  ssin  3431  ssddif  3443  reldisj  3548  ssdif0im  3561  inssdif0im  3564  ssundifim  3580  sbcssg  3605  pwss  3672  snssOLD  3803  snssb  3811  snsssn  3849  ssuni  3920  unissb  3928  intss  3954  iunss  4016  dftr2  4194  axpweq  4267  axpow2  4272  ssextss  4318  ordunisuc2r  4618  setind  4643  zfregfr  4678  tfi  4686  ssrel  4820  ssrel2  4822  ssrelrel  4832  reliun  4854  relop  4886  issref  5126  funimass4  5705  isprm2  12750  bj-inf2vnlem3  16668  bj-inf2vnlem4  16669