Theorem dfdm4 5909

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 3482	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3482	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5896	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1845	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2807	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5902	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5699	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2774	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1537  ∃wex 1776  {cab 2712   class class class wbr 5148  ^◡ccnv 5688  dom cdm 5689  ran crn 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  dmcnvcnv  5947  rncnvcnv  5948  rncoeq  5993  cnvimass  6102  cnvimarndm  6103  dminxp  6202  cnvsn0  6232  rnsnopg  6243  dmmpt  6262  dmco  6276  cores2  6281  cnvssrndm  6293  unidmrn  6301  dfdm2  6303  funimacnv  6649  foimacnv  6866  funcocnv2  6874  f1opw2  7688  cnvexg  7947  tz7.48-3  8483  fopwdom  9119  sbthlem4  9125  fodomr  9167  cnvfi  9215  fodomfir  9366  f1opwfi  9394  zorn2lem4  10537  trclublem  15031  relexpcnv  15071  unbenlem  16942  gsumpropd2lem  18705  pjdm  21745  paste  23318  hmeores  23795  icchmeo  24985  icchmeoOLD  24986  fcnvgreu  32690  ffsrn  32747  gsummpt2co  33034  tocycfvres1  33113  tocycfvres2  33114  cycpmfvlem  33115  cycpmfv3  33118  coinfliprv  34464  itg2addnclem2  37659  rncnv  38282  lnmlmic  43077  dmnonrel  43580  cnvrcl0  43615  conrel1d  43653