Theorem ssalel 3235

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 3234	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3226	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2249	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2347	. . 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 393	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1523	. 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 1400   = wceq 1402   e. wcel 2209   {cab 2224   i^i cin 3219   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  dfss3  3236  dfssf  3238  dfss2f  3239  ssel  3242  ssriv  3252  ssrdv  3254  sstr2  3255  eqss  3263  nssr  3308  rabss2  3331  ssconb  3362  ssequn1  3399  unss  3403  ssin  3453  ssddif  3465  reldisj  3576  ssdif0im  3589  inssdif0imOLD  3593  ssundifim  3611  sbcssg  3636  pwss  3707  snssOLD  3838  snssb  3846  snsssn  3884  ssuni  3955  unissb  3963  intss  3989  iunss  4051  dftr2  4229  axpweq  4306  axpow2  4311  ssextss  4358  ordunisuc2r  4659  setind  4684  zfregfr  4719  tfi  4727  ssrel  4861  ssrel2  4863  ssrelrel  4873  reliun  4896  relop  4928  issref  5168  funimass4  5750  isprm2  12878  bj-inf2vnlem3  16981  bj-inf2vnlem4  16982