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 )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1400   e. wcel 2209   A.wral 2528   C_ wss 3220

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 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 theorem 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 referenced by:  ssrab  3326  eqsnm  3875  uni0b  3955  uni0c  3956  ssint  3981  ssiinf  4057  sspwuni  4092  dftr3  4228  tfis  4725  rninxp  5226  fnres  5495  eqfnfv3  5799  funimass3  5816  ffvresb  5862  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  exmidontriimlem3  7569  suplocsr  8166  4sqlem19  13166  imasaddfnlemg  13612  isbasis2g  15069  tgval2  15075  eltg2b  15078  tgss2  15103  basgen2  15105  bastop1  15107  unicld  15140  neipsm  15178  ssidcn  15234  bdss  16804