Theorem eldm2 3304

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 3303	. 2 |- (A e. dom B <-> E.y ABy)
3		df-br 2616	. . 3 |- (ABy <-> <.A, y>. e. B)
4	3	exbii 1050	. 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 957  E.wex 979  Vcvv 1808  <.cop 2408   class class class wbr 2615  dom cdm 3166

This theorem is referenced by:  eldm2g 3305  dmss 3306  opeldm 3310  dmun 3313  dmin 3314  dmuni 3315  reldm0 3327  dmrnssfld 3353  dmcosseq 3361  dmres 3376  iss 3393  relssdr 3509  dffun7 3536  funssres 3548  fn0 3601  dmfco 3768  tfrlem9 3914  1st2val 4088  tz9.12lem3 4644  cnlnssadj 9969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-un 2047  df-sn 2409  df-pr 2410  df-op 2413  df-br 2616  df-dm 3184

Copyright terms: Public domain