Theorem dfdm4 5793

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 3426	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3426	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5780	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1851	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2809	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5786	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5590	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2777	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1539  ∃wex 1783  {cab 2715   class class class wbr 5070  ^◡ccnv 5579  dom cdm 5580  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  dmcnvcnv  5831  rncnvcnv  5832  rncoeq  5873  cnvimass  5978  cnvimarndm  5979  dminxp  6072  cnvsn0  6102  rnsnopg  6113  dmmpt  6132  dmco  6147  cores2  6152  cnvssrndm  6163  unidmrn  6171  dfdm2  6173  funimacnv  6499  foimacnv  6717  funcocnv2  6724  fimacnvOLD  6930  f1opw2  7502  cnvexg  7745  tz7.48-3  8245  fopwdom  8820  sbthlem4  8826  fodomr  8864  cnvfi  8924  f1opwfi  9053  zorn2lem4  10186  trclublem  14634  relexpcnv  14674  unbenlem  16537  gsumpropd2lem  18278  pjdm  20824  paste  22353  hmeores  22830  icchmeo  24010  fcnvgreu  30912  ffsrn  30966  gsummpt2co  31210  tocycfvres1  31279  tocycfvres2  31280  cycpmfvlem  31281  cycpmfv3  31284  coinfliprv  32349  itg2addnclem2  35756  rncnv  36363  lnmlmic  40829  dmnonrel  41087  cnvrcl0  41122  conrel1d  41160