Theorem dfdm4 5871

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 3458	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3458	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5854	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1868	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2829	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5864	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5657	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2796	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1560  ∃wex 1799  {cab 2740   class class class wbr 5100  ^◡ccnv 5646  dom cdm 5647  ran crn 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is referenced by:  dmcnvcnv  5909  rncnvcnv  5910  rncoeq  5958  cnvimass  6071  cnvimarndm  6072  dminxp  6166  cnvsn0  6197  rnsnopg  6208  dmmpt  6227  dmco  6242  cores2  6247  cnvssrndm  6258  unidmrn  6266  dfdm2  6268  funimacnv  6602  foimacnv  6824  funcocnv2  6832  f1opw2  7651  cnvexg  7905  tz7.48-3  8415  fopwdom  9057  sbthlem4  9062  fodomr  9100  cnvfi  9144  fodomfir  9272  f1opwfi  9299  zorn2lem4  10456  trclublem  15008  relexpcnv  15048  unbenlem  16944  gsumpropd2lem  18713  pjdm  21759  paste  23354  hmeores  23831  icchmeo  25003  fcnvgreu  32874  ffsrn  32930  gsummpt2co  33228  tocycfvres1  33290  tocycfvres2  33291  cycpmfvlem  33292  cycpmfv3  33295  coinfliprv  34780  itg2addnclem2  38171  rncnv  38805  lnmlmic  43665  dmnonrel  44166  cnvrcl0  44201  conrel1d  44239