Theorem dfdm4 5837

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 3435	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3435	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5824	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1855	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2806	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5830	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5628	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2773	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1547  ∃wex 1786  {cab 2717   class class class wbr 5072  ^◡ccnv 5617  dom cdm 5618  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  dmcnvcnv  5875  rncnvcnv  5876  rncoeq  5924  cnvimass  6034  cnvimarndm  6035  dminxp  6131  cnvsn0  6161  rnsnopg  6172  dmmpt  6191  dmco  6206  cores2  6211  cnvssrndm  6222  unidmrn  6230  dfdm2  6232  funimacnv  6566  foimacnv  6784  funcocnv2  6792  f1opw2  7611  cnvexg  7864  tz7.48-3  8373  fopwdom  9013  sbthlem4  9018  fodomr  9056  cnvfi  9100  fodomfir  9228  f1opwfi  9256  zorn2lem4  10412  trclublem  14948  relexpcnv  14988  unbenlem  16870  gsumpropd2lem  18638  pjdm  21682  paste  23277  hmeores  23754  icchmeo  24926  fcnvgreu  32764  ffsrn  32820  gsummpt2co  33129  tocycfvres1  33191  tocycfvres2  33192  cycpmfvlem  33193  cycpmfv3  33196  coinfliprv  34667  itg2addnclem2  38039  rncnv  38673  lnmlmic  43533  dmnonrel  44034  cnvrcl0  44069  conrel1d  44107