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  3575  ssdif0im  3588  inssdif0im  3591  ssundifim  3608  sbcssg  3633  pwss  3704  snssOLD  3835  snssb  3843  snsssn  3881  ssuni  3952  unissb  3960  intss  3986  iunss  4048  dftr2  4226  axpweq  4303  axpow2  4308  ssextss  4355  ordunisuc2r  4656  setind  4681  zfregfr  4716  tfi  4724  ssrel  4858  ssrel2  4860  ssrelrel  4870  reliun  4893  relop  4925  issref  5165  funimass4  5747  isprm2  12873  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913