MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfdm4 Structured version   Visualization version   GIF version

Theorem dfdm4 5225
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.
StepHypRef Expression
1 vex 3175 . . . . 5 𝑦 ∈ V
2 vex 3175 . . . . 5 𝑥 ∈ V
31, 2brcnv 5215 . . . 4 (𝑦𝐴𝑥𝑥𝐴𝑦)
43exbii 1763 . . 3 (∃𝑦 𝑦𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
54abbii 2725 . 2 {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6 dfrn2 5221 . 2 ran 𝐴 = {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥}
7 df-dm 5038 . 2 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
85, 6, 73eqtr4ri 2642 1 dom 𝐴 = ran 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wex 1694  {cab 2595   class class class wbr 4577  ccnv 5027  dom cdm 5028  ran crn 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-cnv 5036  df-dm 5038  df-rn 5039
This theorem is referenced by:  dmcnvcnv  5256  rncnvcnv  5257  rncoeq  5297  cnvimass  5391  cnvimarndm  5392  dminxp  5479  cnvsn0  5507  rnsnopg  5518  dmmpt  5533  dmco  5546  cores2  5551  cnvssrndm  5560  unidmrn  5568  dfdm2  5570  funimacnv  5870  foimacnv  6052  funcocnv2  6059  fimacnv  6240  f1opw2  6764  cnvexg  6983  tz7.48-3  7404  fopwdom  7931  sbthlem4  7936  fodomr  7974  f1opwfi  8131  zorn2lem4  9182  trclublem  13531  relexpcnv  13572  unbenlem  15399  gsumpropd2lem  17045  pjdm  19818  paste  20856  hmeores  21332  icchmeo  22496  fcnvgreu  28689  ffsrn  28726  gsummpt2co  28945  coinfliprv  29705  itg2addnclem2  32456  lnmlmic  36500  dmnonrel  36739  cnvrcl0  36775  conrel1d  36798
  Copyright terms: Public domain W3C validator