Theorem dfss2 3169

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 3168	. . 3 |- ( A C_ B <-> A = ( A i^i B ) )
2		df-in 3160	. . . 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 3153   C_ wss 3154

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 3160  df-ss 3167

This theorem is referenced by:  dfss3  3170  dfss2f  3171  ssel  3174  ssriv  3184  ssrdv  3186  sstr2  3187  eqss  3195  nssr  3240  rabss2  3263  ssconb  3293  ssequn1  3330  unss  3334  ssin  3382  ssddif  3394  reldisj  3499  ssdif0im  3512  inssdif0im  3515  ssundifim  3531  sbcssg  3556  pwss  3618  snssOLD  3745  snssb  3752  snsssn  3788  ssuni  3858  unissb  3866  intss  3892  iunss  3954  dftr2  4130  axpweq  4201  axpow2  4206  ssextss  4250  ordunisuc2r  4547  setind  4572  zfregfr  4607  tfi  4615  ssrel  4748  ssrel2  4750  ssrelrel  4760  reliun  4781  relop  4813  issref  5049  funimass4  5608  isprm2  12258  bj-inf2vnlem3  15534  bj-inf2vnlem4  15535