Theorem ssalel 3213

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 3212	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3204	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2240	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2338	. . 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 1516	. 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 1393   = wceq 1395   e. wcel 2200   {cab 2215   i^i cin 3197   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  dfss3  3214  dfss2f  3216  ssel  3219  ssriv  3229  ssrdv  3231  sstr2  3232  eqss  3240  nssr  3285  rabss2  3308  ssconb  3338  ssequn1  3375  unss  3379  ssin  3427  ssddif  3439  reldisj  3544  ssdif0im  3557  inssdif0im  3560  ssundifim  3576  sbcssg  3601  pwss  3666  snssOLD  3797  snssb  3804  snsssn  3842  ssuni  3913  unissb  3921  intss  3947  iunss  4009  dftr2  4187  axpweq  4259  axpow2  4264  ssextss  4310  ordunisuc2r  4610  setind  4635  zfregfr  4670  tfi  4678  ssrel  4812  ssrel2  4814  ssrelrel  4824  reliun  4846  relop  4878  issref  5117  funimass4  5692  isprm2  12682  bj-inf2vnlem3  16517  bj-inf2vnlem4  16518