Theorem dfss3 3132

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 3131	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2449	. 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 1341   e. wcel 2136   A.wral 2444   C_ wss 3116

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-ral 2449  df-in 3122  df-ss 3129

This theorem is referenced by:  ssrab  3220  eqsnm  3735  uni0b  3814  uni0c  3815  ssint  3840  ssiinf  3915  sspwuni  3950  dftr3  4084  tfis  4560  rninxp  5047  fnres  5304  eqfnfv3  5585  funimass3  5601  ffvresb  5648  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  exmidontriimlem3  7179  suplocsr  7750  isbasis2g  12683  tgval2  12691  eltg2b  12694  tgss2  12719  basgen2  12721  bastop1  12723  unicld  12756  neipsm  12794  ssidcn  12850  bdss  13746