Theorem dfdm4 5879

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 3454	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5862	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1881	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2827	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5872	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5665	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2794	1 ⊢ dom 𝐴 = ran ◡𝐴

This proof depends on syntax axioms:   = wceq 1570  ∃wex 1812  {cab 2738   class class class wbr 5103  ^◡ccnv 5654  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  dmcnvcnv  5917  rncnvcnv  5918  rncoeq  5965  cnvimass  6078  cnvimarndm  6079  dminxp  6173  cnvsn0  6206  rnsnopg  6217  dmmpt  6236  dmco  6251  cores2  6256  cnvssrndm  6268  unidmrn  6277  dfdm2  6279  funimacnv  6615  foimacnv  6836  funcocnv2  6844  f1opw2  7670  cnvexg  7922  tz7.48-3  8436  fopwdom  9086  sbthlem4  9091  fodomr  9129  cnvfi  9173  fodomfir  9300  f1opwfi  9326  zorn2lem4  10504  trclublem  15071  relexpcnv  15111  unbenlem  17003  gsumpropd2lem  18784  pjdm  21923  paste  23522  hmeores  24000  icchmeo  25172  fcnvgreu  33148  ffsrn  33202  gsummpt2co  33491  tocycfvres1  33553  tocycfvres2  33554  cycpmfvlem  33555  cycpmfv3  33558  coinfliprv  34997  itg2addnclem2  38424  rncnv  39057  lnmlmic  43932  dmnonrel  44433  cnvrcl0  44468  conrel1d  44506