Theorem dfss3 3236

Description: Alternate definition of subclass relationship. (Contributed by NM, 14-Oct-1999.)

Assertion

Ref	Expression
dfss3	|- ( A C_ B <-> A. x e. A x e. B )

Distinct variable groups:   x, A   x, B

Proof of Theorem dfss3

Step	Hyp	Ref	Expression
1		ssalel 3235	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2533	. 2 |- ( A. x e. A x e. B <-> A. x ( x e. A -> x e. B ) )
3	1, 2	bitr4i 187	1 |- ( A C_ B <-> A. x e. A x e. B )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400   e. wcel 2209   A.wral 2528   C_ wss 3220

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-ral 2533  df-in 3226  df-ss 3233

This theorem is used by:  ssrab  3326  eqsnm  3880  uni0b  3960  uni0c  3961  ssint  3986  ssiinf  4062  sspwuni  4097  dftr3  4235  tfis  4732  rninxp  5234  fnres  5503  eqfnfv3  5811  funimass3  5828  ffvresb  5874  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  exmidontriimlem3  7585  suplocsr  8182  4sqlem19  13217  imasaddfnlemg  13694  isbasis2g  15271  tgval2  15277  eltg2b  15280  tgss2  15305  basgen2  15307  bastop1  15309  unicld  15342  neipsm  15380  ssidcn  15436  bdss  17095