Theorem dfdm4 5878

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 5861	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1880	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2827	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5871	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5661	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2794	1 ⊢ dom 𝐴 = ran ◡𝐴

This proof depends on syntax axioms:   = wceq 1569  ∃wex 1811  {cab 2738   class class class wbr 5102  ^◡ccnv 5650  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  dmcnvcnv  5916  rncnvcnv  5917  rncoeq  5964  cnvimassrndm  6081  cnvimarndmOLD  6083  dminxp  6174  cnvimass  6201  cnvsn0  6214  rnsnopg  6225  dmmpt  6244  dmco  6259  cores2  6264  cnvssrndm  6276  unidmrn  6285  dfdm2  6287  funimacnv  6626  foimacnv  6847  funcocnv2  6855  f1opw2  7680  cnvexg  7940  tz7.48-3  8462  fopwdom  9112  sbthlem4  9117  fodomr  9155  cnvfi  9199  fodomfir  9327  f1opwfi  9353  zorn2lem4  10584  trclublem  15157  relexpcnv  15197  unbenlem  17095  gsumpropd2lem  18877  pjdm  22022  paste  23621  hmeores  24099  icchmeo  25271  fcnvgreu  33317  ffsrn  33370  gsummpt2co  33659  tocycfvres1  33721  tocycfvres2  33722  cycpmfvlem  33723  cycpmfv3  33726  coinfliprv  35165  j0ltalephlem  35958  itg2addnclem2  38727  rncnv  39375  lnmlmic  44227  dmnonrel  44727  cnvrcl0  44762  conrel1d  44800  cocanss1  46060