Theorem dfss3 3082

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 3081	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2419	. 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 1329   e. wcel 1480   A.wral 2414   C_ wss 3066

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-ral 2419  df-in 3072  df-ss 3079

This theorem is referenced by:  ssrab  3170  eqsnm  3677  uni0b  3756  uni0c  3757  ssint  3782  ssiinf  3857  sspwuni  3892  dftr3  4025  tfis  4492  rninxp  4977  fnres  5234  eqfnfv3  5513  funimass3  5529  ffvresb  5576  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  suplocsr  7610  isbasis2g  12201  tgval2  12209  eltg2b  12212  tgss2  12237  basgen2  12239  bastop1  12241  unicld  12274  neipsm  12312  ssidcn  12368  bdss  13051