Theorem dfss2 3145

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 3144	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3136	. . . 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 3129   C_ wss 3130

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 3136  df-ss 3143

This theorem is referenced by:  dfss3  3146  dfss2f  3147  ssel  3150  ssriv  3160  ssrdv  3162  sstr2  3163  eqss  3171  nssr  3216  rabss2  3239  ssconb  3269  ssequn1  3306  unss  3310  ssin  3358  ssddif  3370  reldisj  3475  ssdif0im  3488  inssdif0im  3491  ssundifim  3507  sbcssg  3533  pwss  3592  snssOLD  3719  snssb  3726  snsssn  3762  ssuni  3832  unissb  3840  intss  3866  iunss  3928  dftr2  4104  axpweq  4172  axpow2  4177  ssextss  4221  ordunisuc2r  4514  setind  4539  zfregfr  4574  tfi  4582  ssrel  4715  ssrel2  4717  ssrelrel  4727  reliun  4748  relop  4778  issref  5012  funimass4  5567  isprm2  12117  bj-inf2vnlem3  14727  bj-inf2vnlem4  14728