Theorem eldm2 3308

Description: Membership in a domain. Theorem 4 of [Suppes] p. 59.

Hypothesis

Ref	Expression
eldm.1	|- A e. V

Assertion

Ref	Expression
eldm2	|- (A e. dom B <-> E.y<.A, y>. e. B)

Distinct variable groups:   y,A   y,B

Proof of Theorem eldm2

Step	Hyp	Ref	Expression
1		eldm.1	. . 3 |- A e. V
2	1	eldm 3307	. 2 |- (A e. dom B <-> E.y ABy)
3		df-br 2620	. . 3 |- (ABy <-> <.A, y>. e. B)
4	3	exbii 1051	. 2 |- (E.y ABy <-> E.y<.A, y>. e. B)
5	2, 4	bitr 173	1 |- (A e. dom B <-> E.y<.A, y>. e. B)

Syntax hints:   <-> wb 146   e. wcel 958  E.wex 980  Vcvv 1811  <.cop 2411   class class class wbr 2619  dom cdm 3170

This theorem is referenced by:  eldm2g 3309  dmss 3310  opeldm 3314  dmun 3317  dmin 3318  dmuni 3319  reldm0 3331  dmrnssfld 3357  dmcosseq 3365  dmres 3380  iss 3397  relssdr 3513  dffun7 3540  funssres 3552  fn0 3605  dmfco 3773  tfrlem9 3919  1st2val 4095  tz9.12lem3 4661  cnlnssadj 10013

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-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-dm 3188

Copyright terms: Public domain