Theorem dfss2 3144

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
dfss2	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 3143	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3135	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2188	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2286	. . 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 1470	. 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 1351   = wceq 1353   e. wcel 2148   {cab 2163   i^i cin 3128   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  dfss3  3145  dfss2f  3146  ssel  3149  ssriv  3159  ssrdv  3161  sstr2  3162  eqss  3170  nssr  3215  rabss2  3238  ssconb  3268  ssequn1  3305  unss  3309  ssin  3357  ssddif  3369  reldisj  3474  ssdif0im  3487  inssdif0im  3490  ssundifim  3506  sbcssg  3532  pwss  3591  snssOLD  3718  snssb  3725  snsssn  3761  ssuni  3831  unissb  3839  intss  3865  iunss  3927  dftr2  4103  axpweq  4171  axpow2  4176  ssextss  4220  ordunisuc2r  4513  setind  4538  zfregfr  4573  tfi  4581  ssrel  4714  ssrel2  4716  ssrelrel  4726  reliun  4747  relop  4777  issref  5011  funimass4  5566  isprm2  12111  bj-inf2vnlem3  14606  bj-inf2vnlem4  14607