Theorem dfdm4 5886

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 3467	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3467	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5869	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1875	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2836	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5879	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5672	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2803	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1567  ∃wex 1806  {cab 2747   class class class wbr 5113  ^◡ccnv 5661  dom cdm 5662  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  dmcnvcnv  5924  rncnvcnv  5925  rncoeq  5972  cnvimass  6085  cnvimarndm  6086  dminxp  6179  cnvsn0  6212  rnsnopg  6223  dmmpt  6242  dmco  6257  cores2  6262  cnvssrndm  6273  unidmrn  6281  dfdm2  6283  funimacnv  6618  foimacnv  6839  funcocnv2  6847  f1opw2  7666  cnvexg  7920  tz7.48-3  8430  fopwdom  9072  sbthlem4  9077  fodomr  9115  cnvfi  9159  fodomfir  9286  f1opwfi  9312  zorn2lem4  10482  trclublem  15031  relexpcnv  15071  unbenlem  16967  gsumpropd2lem  18736  pjdm  21825  paste  23419  hmeores  23896  icchmeo  25068  fcnvgreu  32957  ffsrn  33013  gsummpt2co  33308  tocycfvres1  33370  tocycfvres2  33371  cycpmfvlem  33372  cycpmfv3  33375  coinfliprv  34817  itg2addnclem2  38210  rncnv  38844  lnmlmic  43706  dmnonrel  44207  cnvrcl0  44242  conrel1d  44280