Theorem dfss2 1497

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 group(s):   x,A   x,B

Proof of Theorem dfss2

Step	Hyp	Ref	Expression
1		dfss 1493	. . 3 |- (A (_ B <-> A = (A i^i B))
2		df-in 1491	. . . 4 |- (A i^i B) = {x | (x e. A /\ x e. B)}
3	2	cleq2i 1111	. . 3 |- (A = (A i^i B) <-> A = {x | (x e. A /\ x e. B)})
4		cleqab 1174	. . 3 |- (A = {x | (x e. A /\ x e. B)} <-> A.x(x e. A <-> (x e. A /\ x e. B)))
5	1, 3, 4	3bitr 155	. 2 |- (A (_ B <-> A.x(x e. A <-> (x e. A /\ x e. B)))
6		pm4.71 481	. . 3 |- ((x e. A -> x e. B) <-> (x e. A <-> (x e. A /\ x e. B)))
7	6	bial 695	. 2 |- (A.x(x e. A -> x e. B) <-> A.x(x e. A <-> (x e. A /\ x e. B)))
8	5, 7	bitr4 154	1 |- (A (_ B <-> A.x(x e. A -> x e. B))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  A.wal 672  {cab 1090   = wceq 1091   e. wcel 1092   i^i cin 1486   (_ wss 1487

This theorem is referenced by:  dfss3 1498  dfss2f 1499  ssel 1502  ssriv 1508  ssrdv 1509  sstr2 1510  eqss 1516  nss 1550  ssconb 1598  unss1 1627  ssequn1 1628  unss 1632  ssrin 1661  disj2 1735  ssdif0 1748  difin0ss 1753  inssdif0 1754  pwex 1806  snss 1849  prsspw 1858  ssextss 1864  pwpw0 1883  ssuni 1937  unissb 1941  intss 1983  iunss 2017  ssiun 2018  ssiin 2024  iinss 2025  dftr2 2043  dfom2 2374  relss 2480  reluni 2493  dmcosseq 2572  inf2 3459  setind2 3493  psslinpr 3929  prlem934 3933  ltaddpr 3934  pjnormss 5638

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org