Theorem dmss 3310

Description: Subset theorem for domain.

Assertion

Ref	Expression
dmss	|- (A (_ B -> dom A (_ dom B)

Proof of Theorem dmss

Step	Hyp	Ref	Expression
1		ssel 2063	. . . 4 |- (A (_ B -> (<.x, y>. e. A -> <.x, y>. e. B))
2	1	19.22dv 1290	. . 3 |- (A (_ B -> (E.y<.x, y>. e. A -> E.y<.x, y>. e. B))
3		visset 1813	. . . 4 |- x e. V
4	3	eldm2 3308	. . 3 |- (x e. dom A <-> E.y<.x, y>. e. A)
5	3	eldm2 3308	. . 3 |- (x e. dom B <-> E.y<.x, y>. e. B)
6	2, 4, 5	3imtr4g 553	. 2 |- (A (_ B -> (x e. dom A -> x e. dom B))
7	6	ssrdv 2070	1 |- (A (_ B -> dom A (_ dom B)

Syntax hints:   -> wi 3   e. wcel 958  E.wex 980   (_ wss 2047  <.cop 2411  dom cdm 3170

This theorem is referenced by:  dmeq 3311  dmv 3327  rnss 3342  ssxpr 3475  funssxp 3638  dff2 3817  tfrlem13 3923  ecopoprdm 4309  dmen 4407  brdom3 4801  brdom5 4802  brdom4 4803  metss 7824  lmsslem 7952  lmss 7953  caussi 7954  causs 7955  dmhmph 10532  reldded 10674  reldcat 10695

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-dm 3188

Copyright terms: Public domain