Theorem dfdm4 5738

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 3402	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3402	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5725	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1854	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2803	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5731	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5535	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2772	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1542  ∃wex 1786  {cab 2716   class class class wbr 5030  ^◡ccnv 5524  dom cdm 5525  ran crn 5526

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pr 5296

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-un 3848  df-nul 4212  df-if 4415  df-sn 4517  df-pr 4519  df-op 4523  df-br 5031  df-opab 5093  df-cnv 5533  df-dm 5535  df-rn 5536

This theorem is referenced by:  dmcnvcnv  5776  rncnvcnv  5777  rncoeq  5818  cnvimass  5923  cnvimarndm  5924  dminxp  6012  cnvsn0  6042  rnsnopg  6053  dmmpt  6072  dmco  6087  cores2  6092  cnvssrndm  6103  unidmrn  6111  dfdm2  6113  funimacnv  6420  foimacnv  6635  funcocnv2  6642  fimacnvOLD  6848  f1opw2  7416  cnvexg  7655  tz7.48-3  8109  fopwdom  8674  sbthlem4  8680  fodomr  8718  cnvfi  8777  f1opwfi  8901  zorn2lem4  9999  trclublem  14444  relexpcnv  14484  unbenlem  16344  gsumpropd2lem  18005  pjdm  20523  paste  22045  hmeores  22522  icchmeo  23693  fcnvgreu  30585  ffsrn  30639  gsummpt2co  30885  tocycfvres1  30954  tocycfvres2  30955  cycpmfvlem  30956  cycpmfv3  30959  coinfliprv  32019  itg2addnclem2  35452  rncnv  36059  lnmlmic  40485  dmnonrel  40743  cnvrcl0  40778  conrel1d  40817