Theorem dfdm4 5885

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 3459	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3459	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5868	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1878	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2830	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5878	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5671	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2797	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1570  ∃wex 1809  {cab 2741   class class class wbr 5109  ^◡ccnv 5660  dom cdm 5661  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  dmcnvcnv  5923  rncnvcnv  5924  rncoeq  5971  cnvimass  6084  cnvimarndm  6085  dminxp  6178  cnvsn0  6211  rnsnopg  6222  dmmpt  6241  dmco  6256  cores2  6261  cnvssrndm  6272  unidmrn  6280  dfdm2  6282  funimacnv  6617  foimacnv  6838  funcocnv2  6846  f1opw2  7665  cnvexg  7917  tz7.48-3  8427  fopwdom  9069  sbthlem4  9074  fodomr  9112  cnvfi  9156  fodomfir  9283  f1opwfi  9309  zorn2lem4  10478  trclublem  15028  relexpcnv  15068  unbenlem  16963  gsumpropd2lem  18732  pjdm  21857  paste  23451  hmeores  23928  icchmeo  25100  fcnvgreu  33017  ffsrn  33073  gsummpt2co  33368  tocycfvres1  33430  tocycfvres2  33431  cycpmfvlem  33432  cycpmfv3  33435  coinfliprv  34873  itg2addnclem2  38343  rncnv  38975  lnmlmic  43835  dmnonrel  44336  cnvrcl0  44371  conrel1d  44409