Theorem dfdm4 5859

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 3451	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3451	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5846	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1848	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2796	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5852	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5648	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2763	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1540  ∃wex 1779  {cab 2707   class class class wbr 5107  ^◡ccnv 5637  dom cdm 5638  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  dmcnvcnv  5897  rncnvcnv  5898  rncoeq  5943  cnvimass  6053  cnvimarndm  6054  dminxp  6153  cnvsn0  6183  rnsnopg  6194  dmmpt  6213  dmco  6227  cores2  6232  cnvssrndm  6244  unidmrn  6252  dfdm2  6254  funimacnv  6597  foimacnv  6817  funcocnv2  6825  f1opw2  7644  cnvexg  7900  tz7.48-3  8412  fopwdom  9049  sbthlem4  9054  fodomr  9092  cnvfi  9140  fodomfir  9279  f1opwfi  9307  zorn2lem4  10452  trclublem  14961  relexpcnv  15001  unbenlem  16879  gsumpropd2lem  18606  pjdm  21616  paste  23181  hmeores  23658  icchmeo  24838  icchmeoOLD  24839  fcnvgreu  32597  ffsrn  32652  gsummpt2co  32988  tocycfvres1  33067  tocycfvres2  33068  cycpmfvlem  33069  cycpmfv3  33072  coinfliprv  34474  itg2addnclem2  37666  rncnv  38288  lnmlmic  43077  dmnonrel  43579  cnvrcl0  43614  conrel1d  43652