Theorem dfss3 3182

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 3181	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2489	. 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 1371   e. wcel 2176   A.wral 2484   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-ral 2489  df-in 3172  df-ss 3179

This theorem is referenced by:  ssrab  3271  eqsnm  3796  uni0b  3875  uni0c  3876  ssint  3901  ssiinf  3977  sspwuni  4012  dftr3  4146  tfis  4631  rninxp  5126  fnres  5392  eqfnfv3  5679  funimass3  5696  ffvresb  5743  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  exmidontriimlem3  7335  suplocsr  7922  4sqlem19  12732  imasaddfnlemg  13146  isbasis2g  14517  tgval2  14523  eltg2b  14526  tgss2  14551  basgen2  14553  bastop1  14555  unicld  14588  neipsm  14626  ssidcn  14682  bdss  15800