Theorem dfss2 3050

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 3049	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3041	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2123	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2221	. . 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 205	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 384	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1427	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 186	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1310   = wceq 1312   e. wcel 1461   {cab 2099   i^i cin 3034   C_ wss 3035

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048

This theorem is referenced by:  dfss3  3051  dfss2f  3052  ssel  3055  ssriv  3065  ssrdv  3067  sstr2  3068  eqss  3076  nssr  3121  rabss2  3144  ssconb  3173  ssequn1  3210  unss  3214  ssin  3262  ssddif  3274  reldisj  3378  ssdif0im  3391  inssdif0im  3394  ssundifim  3410  sbcssg  3436  pwss  3490  snss  3613  snsssn  3652  ssuni  3722  unissb  3730  intss  3756  iunss  3818  dftr2  3986  axpweq  4053  axpow2  4058  ssextss  4100  ordunisuc2r  4388  setind  4412  zfregfr  4446  tfi  4454  ssrel  4585  ssrel2  4587  ssrelrel  4597  reliun  4618  relop  4647  issref  4877  funimass4  5424  isprm2  11637  bj-inf2vnlem3  12849  bj-inf2vnlem4  12850