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  8434  fopwdom  9084  sbthlem4  9089  fodomr  9127  cnvfi  9171  fodomfir  9298  f1opwfi  9324  zorn2lem4  10502  trclublem  15069  relexpcnv  15109  unbenlem  17001  gsumpropd2lem  18782  pjdm  21921  paste  23520  hmeores  23998  icchmeo  25170  fcnvgreu  33146  ffsrn  33200  gsummpt2co  33489  tocycfvres1  33551  tocycfvres2  33552  cycpmfvlem  33553  cycpmfv3  33556  coinfliprv  34995  itg2addnclem2  38422  rncnv  39055  lnmlmic  43930  dmnonrel  44431  cnvrcl0  44466  conrel1d  44504