Theorem dfss2 3168

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 3167	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3159	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i 2204	. . 3 |- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2 2302	. . 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 206	. 2 |- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71 389	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii 1481	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5, 7	bitr4i 187	1 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1362   = wceq 1364   e. wcel 2164   {cab 2179   i^i cin 3152   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  dfss3  3169  dfss2f  3170  ssel  3173  ssriv  3183  ssrdv  3185  sstr2  3186  eqss  3194  nssr  3239  rabss2  3262  ssconb  3292  ssequn1  3329  unss  3333  ssin  3381  ssddif  3393  reldisj  3498  ssdif0im  3511  inssdif0im  3514  ssundifim  3530  sbcssg  3555  pwss  3617  snssOLD  3744  snssb  3751  snsssn  3787  ssuni  3857  unissb  3865  intss  3891  iunss  3953  dftr2  4129  axpweq  4200  axpow2  4205  ssextss  4249  ordunisuc2r  4546  setind  4571  zfregfr  4606  tfi  4614  ssrel  4747  ssrel2  4749  ssrelrel  4759  reliun  4780  relop  4812  issref  5048  funimass4  5607  isprm2  12255  bj-inf2vnlem3  15464  bj-inf2vnlem4  15465