Theorem dfss2 2029

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 2025	. . 3 |- (A (_ B <-> A = (A i^i B))
2		df-in 2022	. . . 4 |- (A i^i B) = {x | (x e. A /\ x e. B)}
3	2	eqeq2i 1461	. . 3 |- (A = (A i^i B) <-> A = {x | (x e. A /\ x e. B)})
4		abeq2 1544	. . 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 177	. 2 |- (A (_ B <-> A.x(x e. A <-> (x e. A /\ x e. B)))
6		pm4.71 633	. . 3 |- ((x e. A -> x e. B) <-> (x e. A <-> (x e. A /\ x e. B)))
7	6	albii 975	. 2 |- (A.x(x e. A -> x e. B) <-> A.x(x e. A <-> (x e. A /\ x e. B)))
8	5, 7	bitr4 176	1 |- (A (_ B <-> A.x(x e. A -> x e. B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 950   = wceq 1099   e. wcel 1105  {cab 1440   i^i cin 2017   (_ wss 2018

This theorem is referenced by:  dfss3 2030  dfss2f 2031  ssel 2034  ssriv 2040  ssrdv 2041  sstr2 2042  eqss 2048  nss 2084  rabss2 2100  ssconb 2141  unss1 2170  ssequn1 2171  unss 2175  ssrin 2205  reldisj 2284  ssdif0 2298  difin0ss 2303  inssdif0 2304  ssundif 2315  snss 2431  pwpw0 2439  prsspw 2450  ssuni 2490  unissb 2496  intss 2522  iunss 2559  ssiun 2560  ssiin 2567  iinss 2568  dftr2 2650  pwex 2713  ssextss 2730  dfom2 3096  ssrel 3209  reluni 3227  dmcosseq 3316  funimass4 3702  inf2 4532  setind2 4573  psslinpr 5058  prlem934 5062  ltaddpr 5063  tgss3t 7531  metcld 7849  grothprim 8635  uninqs 8701  hst1 8811  pjnormss 10221

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-in 2022  df-ss 2024

Copyright terms: Public domain