Theorem dfss3 3146

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 3145	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2		df-ral 2460	. 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 1351   e. wcel 2148   A.wral 2455   C_ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ral 2460  df-in 3136  df-ss 3143

This theorem is referenced by:  ssrab  3234  eqsnm  3756  uni0b  3835  uni0c  3836  ssint  3861  ssiinf  3937  sspwuni  3972  dftr3  4106  tfis  4583  rninxp  5073  fnres  5333  eqfnfv3  5616  funimass3  5633  ffvresb  5680  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  exmidontriimlem3  7222  suplocsr  7808  imasaddfnlemg  12735  isbasis2g  13548  tgval2  13554  eltg2b  13557  tgss2  13582  basgen2  13584  bastop1  13586  unicld  13619  neipsm  13657  ssidcn  13713  bdss  14619