Theorem dfss3 3157

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 3156	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2470	. 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 )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1361   e. wcel 2158   A.wral 2465   C_ wss 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-ral 2470  df-in 3147  df-ss 3154

This theorem is referenced by:  ssrab  3245  eqsnm  3767  uni0b  3846  uni0c  3847  ssint  3872  ssiinf  3948  sspwuni  3983  dftr3  4117  tfis  4594  rninxp  5084  fnres  5344  eqfnfv3  5628  funimass3  5645  ffvresb  5692  tfrlemibxssdm  6342  tfr1onlembxssdm  6358  tfrcllembxssdm  6371  exmidontriimlem3  7236  suplocsr  7822  imasaddfnlemg  12753  isbasis2g  13841  tgval2  13847  eltg2b  13850  tgss2  13875  basgen2  13877  bastop1  13879  unicld  13912  neipsm  13950  ssidcn  14006  bdss  14912