Theorem rneqd 5219

Description: Equality deduction for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
rneqd	|- ( ph -> ran A = ran B )

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 |- ( ph -> A = B )
2		rneq 5217	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	syl 16	1 |- ( ph -> ran A = ran B )

Syntax hints:   -> wi 4   = wceq 1398   ran crn 4989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-cnv 4996  df-dm 4998  df-rn 4999

This theorem is referenced by:  resima2  5295  imaeq1  5320  imaeq2  5321  resiima  5339  rnxpid  5425  xpima  5434  funimacnv  5642  fnima  5681  elxp4  6717  elxp5  6718  2ndval  6776  fo2nd  6794  f2ndres  6796  curry1  6865  curry2  6868  oarec  7203  en1  7575  xpassen  7604  xpdom2  7605  sbthlem4  7623  fodomr  7661  dffi3  7883  marypha2lem4  7890  ordtypelem9  7943  dfac12lem1  8514  dfac12r  8517  fin23lem32  8715  fin23lem34  8717  fin23lem35  8718  fin23lem36  8719  fin23lem38  8720  fin23lem39  8721  fin23lem41  8723  itunitc  8792  ttukeylem3  8882  fpwwe2lem6  9002  fpwwe2lem9  9005  wunex2  9105  wuncval2  9114  gruima  9169  rpnnen1  11214  hashf1lem1  12491  s1rn  12603  relexprng  12964  relexpfld  12967  limsupval  13382  xpnnenOLD  14030  vdwapfval  14576  vdwapval  14578  vdwmc  14583  vdwpc  14585  vdwlem6  14591  vdwlem8  14593  restval  14919  restid2  14923  prdsval  14947  prdsdsval  14970  prdsdsval2  14976  prdsdsval3  14977  imasval  15003  imasdsval  15007  isfull  15401  arwval  15524  gsumvalx  16099  conjsubg  16500  pmtrfrn  16685  psgnfval  16727  sylow1lem2  16821  sylow1lem4  16823  sylow1  16825  sylow2blem1  16842  sylow2b  16845  sylow3lem1  16849  sylow3lem2  16850  sylow3lem3  16851  sylow3lem5  16853  sylow3lem6  16854  sylow3  16855  lsmfval  16860  lsmvalx  16861  oppglsm  16864  subglsm  16893  lsmpropd  16897  efgval2  16944  efgi2  16945  efgtlen  16946  efgsdm  16950  efgsdmi  16952  efgsrel  16954  efgs1b  16956  efgsp1  16957  efgsres  16958  efgsfo  16959  efgrelexlemb  16970  frgpnabllem1  17079  iscyg  17084  iscyggen  17085  gsumxp  17203  dprdval  17232  dprdvalOLD  17234  ablfac2  17338  evlseu  18383  zncyg  18763  cygznlem2a  18782  frlmsplit2  18977  tgrest  19830  ordtval  19860  ordtbas2  19862  ordtcnv  19872  ordtrest  19873  ordtrest2  19875  ispnrm  20010  cmpfi  20078  txval  20234  xkoval  20257  ptval2  20271  ptpjopn  20282  xkoccn  20289  xkoptsub  20324  xkopt  20325  fmval  20613  fmf  20615  txflf  20676  cnextf  20735  subgntr  20774  opnsubg  20775  clsnsg  20777  snclseqg  20783  tsmsval2  20797  tsmsxplem1  20824  ustuqtoplem  20911  utopsnneiplem  20919  utopsnneip  20920  fmucndlem  20963  ressprdsds  21043  mopnval  21110  metuvalOLD  21221  metuval  21222  metdsval  21520  lebnumlem1  21630  lebnumlem3  21632  pi1xfrcnvlem  21725  pi1xfrcnv  21726  minveclem3b  22012  elovolmr  22056  ovolctb  22070  ovoliunlem3  22084  ovolshftlem1  22089  voliunlem3  22131  voliun  22133  volsup  22135  uniioombllem2  22161  uniioombllem3  22163  mbflimsup  22242  itg1climres  22290  itg2monolem1  22326  itg2i1fseq  22331  itg2cnlem1  22337  ellimc2  22450  dvivth  22580  dvne0  22581  lhop2  22585  lhop  22586  mdegfval  22629  dchrptlem2  23741  dchrpt  23743  tglnunirn  24139  tgisline  24211  perpln1  24291  perpln2  24292  isperp  24293  ishpg  24332  lmif  24355  islmib  24357  edgval  24544  edgopval  24545  edgss  24557  nbgraop  24628  nbgraopALT  24629  ex-ima  25368  subgornss  25509  efghgrpOLD  25576  isrngo  25581  drngoi  25610  vcoprne  25673  bafval  25698  pj3i  27328  ofrn2  27704  ffsrn  27786  ordtprsval  28138  ordtprsuni  28139  ordtcnvNEW  28140  ordtrestNEW  28141  ordtrest2NEW  28143  qqhval  28192  qqhval2  28200  esumval  28278  esumsnf  28296  esumrnmpt2  28300  esumfsupre  28303  esumsup  28321  sxval  28401  omsval  28504  omsfval  28505  carsggect  28529  sibf0  28543  sitgfval  28550  cvmlift3lem6  29036  mvtval  29127  mvrsval  29132  mrsubrn  29140  mrsub0  29143  mrsubf  29144  mrsubccat  29145  mrsubcn  29146  mrsubco  29148  mrsubvrs  29149  elmsubrn  29155  msubrn  29156  msubf  29159  mstaval  29171  msubvrs  29187  mclsval  29190  trpredeq1  29546  trpredeq2  29547  trpredeq3  29548  mblfinlem2  30295  ovoliunnfl  30299  voliunnfl  30301  filnetlem4  30442  rngohomval  30610  rngoisoval  30623  idlval  30653  pridlval  30673  maxidlval  30679  igenval  30701  mzpmfp  30922  eldiophb  30932  diophrw  30934  fourierdlem60  32191  fourierdlem61  32192  fnrnafv  32489  csbima12gALTOLD  34041  lsatset  35131  docaffvalN  37264  docafvalN  37265  conrel1d  38195  iunrelexp0  38245