Theorem dfss2 2110

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17.

Assertion

Ref	Expression
dfss2	|- (A (_ 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 2106	. . 3 |- (A (_ B <-> A = (A i^i B))
2		df-in 2103	. . . 4 |- (A i^i B) = {x | (x e. A /\ x e. B)}
3	2	eqeq2i 1528	. . 3 |- (A = (A i^i B) <-> A = {x | (x e. A /\ x e. B)})
4		abeq2 1611	. . 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 175	. 2 |- (A (_ B <-> A.x(x e. A <-> (x e. A /\ x e. B)))
6		pm4.71 638	. . 3 |- ((x e. A -> x e. B) <-> (x e. A <-> (x e. A /\ x e. B)))
7	6	albii 1035	. 2 |- (A.x(x e. A -> x e. B) <-> A.x(x e. A <-> (x e. A /\ x e. B)))
8	5, 7	bitr4i 174	1 |- (A (_ B <-> A.x(x e. A -> x e. B))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994  {cab 1505   i^i cin 2098   (_ wss 2099

This theorem is referenced by:  dfss3 2111  dfss2f 2112  ssel 2115  ssriv 2121  ssrdv 2122  sstr2 2123  eqss 2129  nss 2165  rabss2 2181  ssconb 2222  unss1 2251  ssequn1 2252  unss 2256  ssrin 2286  reldisj 2366  ssdif0 2380  difin0ss 2385  inssdif0 2386  ssundif 2398  pwss 2466  snss 2525  pwpw0 2533  prsspw 2545  pwsnALT 2566  ssuni 2589  unissb 2595  intss 2621  iunss 2659  ssiun 2660  ssiin 2667  iinss 2668  dftr2 2756  axpweq 2817  axpow2 2820  pwex 2823  ssextss 2839  dfom2 3220  ssrel 3334  ssrelrel 3340  reliun 3354  relop 3365  dmcosseq 3452  funimass4 3874  inf2 4753  setind2 4795  psslinpr 5289  prlem934 5293  ltaddpr 5294  tgss3 7850  metcld 8178  grothpw 9054  grothprim 9057  pjnormssi 10376  uninqs 10730  ref3w 10772  hst1 11109  bwt2 11123  usinuniop 11128  neibastop2lem3 11582  limfilcf 11683  fcluscf 11724  gafo 11773

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain