Theorem dfss2 2934

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 2932	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 2924	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2050	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2146	. . 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 195	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 369	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1359	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 176	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   A.wal 1241   = wceq 1243   e. wcel 1393   {cab 2026   i^i cin 2916   C_ wss 2917

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931

This theorem is referenced by:  dfss3  2935  dfss2f  2936  ssel  2939  ssriv  2949  ssrdv  2951  sstr2  2952  eqss  2960  nssr  3003  rabss2  3023  ssconb  3076  ssequn1  3113  unss  3117  ssin  3159  ssddif  3171  reldisj  3271  ssdif0im  3286  inssdif0im  3291  ssundifim  3306  sbcssg  3330  pwss  3374  snss  3494  snsssn  3532  ssuni  3602  unissb  3610  intss  3636  iunss  3698  dftr2  3856  axpweq  3924  axpow2  3929  ssextss  3956  ordunisuc2r  4240  setind  4264  zfregfr  4298  tfi  4305  ssrel  4428  ssrel2  4430  ssrelrel  4440  reliun  4458  relop  4486  issref  4707  funimass4  5224  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098