Theorem dfdm4 5728

Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)

Assertion

Ref	Expression
dfdm4	⊢ dom 𝐴 = ran ◡𝐴

Proof of Theorem dfdm4

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3444	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3444	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5717	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1849	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2863	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5723	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5529	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2832	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1538  ∃wex 1781  {cab 2776   class class class wbr 5030  ^◡ccnv 5518  dom cdm 5519  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  dmcnvcnv  5767  rncnvcnv  5768  rncoeq  5811  cnvimass  5916  cnvimarndm  5917  dminxp  6004  cnvsn0  6034  rnsnopg  6045  dmmpt  6061  dmco  6074  cores2  6079  cnvssrndm  6090  unidmrn  6098  dfdm2  6100  funimacnv  6405  foimacnv  6607  funcocnv2  6614  fimacnv  6816  f1opw2  7380  cnvexg  7611  tz7.48-3  8063  fopwdom  8608  sbthlem4  8614  fodomr  8652  f1opwfi  8812  zorn2lem4  9910  trclublem  14346  relexpcnv  14386  unbenlem  16234  gsumpropd2lem  17881  pjdm  20396  paste  21899  hmeores  22376  icchmeo  23546  fcnvgreu  30436  ffsrn  30491  gsummpt2co  30733  tocycfvres1  30802  tocycfvres2  30803  cycpmfvlem  30804  cycpmfv3  30807  coinfliprv  31850  itg2addnclem2  35109  rncnv  35718  lnmlmic  40032  dmnonrel  40290  cnvrcl0  40325  conrel1d  40364