Theorem dfdm4 5880

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 3468	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3468	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5867	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1848	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2803	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5873	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5669	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2770	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1540  ∃wex 1779  {cab 2714   class class class wbr 5124  ^◡ccnv 5658  dom cdm 5659  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  dmcnvcnv  5918  rncnvcnv  5919  rncoeq  5964  cnvimass  6074  cnvimarndm  6075  dminxp  6174  cnvsn0  6204  rnsnopg  6215  dmmpt  6234  dmco  6248  cores2  6253  cnvssrndm  6265  unidmrn  6273  dfdm2  6275  funimacnv  6622  foimacnv  6840  funcocnv2  6848  f1opw2  7667  cnvexg  7925  tz7.48-3  8463  fopwdom  9099  sbthlem4  9105  fodomr  9147  cnvfi  9195  fodomfir  9345  f1opwfi  9373  zorn2lem4  10518  trclublem  15019  relexpcnv  15059  unbenlem  16933  gsumpropd2lem  18662  pjdm  21672  paste  23237  hmeores  23714  icchmeo  24894  icchmeoOLD  24895  fcnvgreu  32656  ffsrn  32711  gsummpt2co  33047  tocycfvres1  33126  tocycfvres2  33127  cycpmfvlem  33128  cycpmfv3  33131  coinfliprv  34520  itg2addnclem2  37701  rncnv  38323  lnmlmic  43087  dmnonrel  43589  cnvrcl0  43624  conrel1d  43662