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  4147  tfis  4632  rninxp  5127  fnres  5394  eqfnfv3  5681  funimass3  5698  ffvresb  5745  tfrlemibxssdm  6415  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  exmidontriimlem3  7337  suplocsr  7924  4sqlem19  12765  imasaddfnlemg  13179  isbasis2g  14550  tgval2  14556  eltg2b  14559  tgss2  14584  basgen2  14586  bastop1  14588  unicld  14621  neipsm  14659  ssidcn  14715  bdss  15837