Theorem dfss2 2988

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)

Assertion

Ref	Expression
dfss2	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Distinct variable groups:   x, A   x, B

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 2987	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 2979	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2091	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2187	. . 3 |- ( A = { x | ( x e. A /\ x e. B ) } <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
5	1, 3, 4	3bitri 204	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 381	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1399	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 185	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   A.wal 1282   = wceq 1284   e. wcel 1433   {cab 2067   i^i cin 2972   C_ wss 2973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  dfss3  2989  dfss2f  2990  ssel  2993  ssriv  3003  ssrdv  3005  sstr2  3006  eqss  3014  nssr  3057  rabss2  3077  ssconb  3105  ssequn1  3142  unss  3146  ssin  3188  ssddif  3198  reldisj  3295  ssdif0im  3308  inssdif0im  3311  ssundifim  3326  sbcssg  3350  pwss  3397  snss  3516  snsssn  3553  ssuni  3623  unissb  3631  intss  3657  iunss  3719  dftr2  3877  axpweq  3945  axpow2  3950  ssextss  3975  ordunisuc2r  4258  setind  4282  zfregfr  4316  tfi  4323  ssrel  4446  ssrel2  4448  ssrelrel  4458  reliun  4476  relop  4504  issref  4727  funimass4  5245  isprm2  10499  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768