Theorem dfss3 3118

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		dfss2 3117	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2440	. 2 |- ( A. x e. A x e. B <-> A. x ( x e. A -> x e. B ) )
3	1, 2	bitr4i 186	1 |- ( A C_ B <-> A. x e. A x e. B )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1333   e. wcel 2128   A.wral 2435   C_ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-ral 2440  df-in 3108  df-ss 3115

This theorem is referenced by:  ssrab  3206  eqsnm  3720  uni0b  3799  uni0c  3800  ssint  3825  ssiinf  3900  sspwuni  3935  dftr3  4069  tfis  4545  rninxp  5032  fnres  5289  eqfnfv3  5570  funimass3  5586  ffvresb  5633  tfrlemibxssdm  6277  tfr1onlembxssdm  6293  tfrcllembxssdm  6306  exmidontriimlem3  7161  suplocsr  7732  isbasis2g  12539  tgval2  12547  eltg2b  12550  tgss2  12575  basgen2  12577  bastop1  12579  unicld  12612  neipsm  12650  ssidcn  12706  bdss  13536