Theorem eleq1d 2419

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
eleq1d	|- (ph -> (A e. C <-> B e. C))

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 |- (ph -> A = B)
2		eleq1 2413	. 2 |- (A = B -> (A e. C <-> B e. C))
3	1, 2	syl 15	1 |- (ph -> (A e. C <-> B e. C))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  eleq12d  2421  eqeltrd  2427  eqneltrd  2446  eqneltrrd  2447  rspcimdv  2957  reuind  3040  sbcel2g  3158  sbccsb2g  3166  ifexg  3722  ninexg  4098  snex  4112  snel1cg  4142  eluni1g  4173  opkelcnvkg  4250  otkelins2kg  4254  otkelins3kg  4255  elimakg  4258  opkelcokg  4262  elp6  4264  opksnelsik  4266  opkelimagekg  4272  elimaksn  4284  xpkvexg  4286  cnvkexg  4287  p6exg  4291  sikexg  4297  dfimak2  4299  ins2kexg  4306  ins3kexg  4307  setswith  4322  ndisjrelk  4324  dfpw2  4328  eqpw1uni  4331  dfaddc2  4382  dfnnc2  4396  peano2  4404  nncaddccl  4420  nnsucelrlem1  4425  nnsucelr  4429  preaddccan2lem1  4455  leltfintr  4459  ltfinex  4465  ltfintrilem1  4466  ltfintri  4467  lenltfin  4470  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinraise  4482  ncfinlowerlem1  4483  ncfinlower  4484  nnpw1ex  4485  eqtfinrelk  4487  tfincl  4493  tfindi  4497  tfinsuc  4499  tfinltfin  4502  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  eventfin  4518  oddtfin  4519  nnadjoinlem1  4520  nnadjoin  4521  nnpweqlem1  4523  nnpweq  4524  srelk  4525  sfin01  4529  sfindbl  4531  sfintfinlem1  4532  tfinnnlem1  4534  tfinnn  4535  sfinltfin  4536  spfinex  4538  1cvsfin  4543  vfintle  4547  vfinncvntnn  4549  vfinspsslem1  4551  vfinspss  4552  vfinspclt  4553  vfinncsp  4555  dfop2lem1  4574  proj1op  4601  proj2op  4602  opeq  4620  breq1  4643  breq2  4644  opelopabsb  4698  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem4  4735  setconslem6  4737  setconslem7  4738  df1st2  4739  dfswap2  4742  dfima2  4746  dfco1  4749  dfsi2  4752  opeliunxp2  4823  ssrel  4845  ssopr  4847  opabid2  4862  opeldm  4911  elimapw12  4946  elimapw13  4947  elimapw11c  4949  elsnres  4997  iss  5001  xpexr  5110  nfunv  5139  ndmfvrcl  5351  respreima  5411  fvelrn  5414  ffnfvf  5429  ffvresb  5432  fsn  5433  fressnfv  5440  funfvima  5460  ffnov  5588  fovcl  5589  funimassov  5610  ndmovcl  5615  ndmovrcl  5617  caovcld  5623  oprabid2  5647  fvmpti  5700  ov2gf  5712  ovmpt2x  5713  fvmptf  5723  fvmptss2  5726  fmpt2x  5731  otelins2  5792  otelins3  5793  oqelins4  5795  txpcofun  5804  clos1exg  5878  mapex  6007  bren  6031  xpassen  6058  ce0nnul  6178  ce0nnuli  6179  ce0addcnnul  6180  cenc  6182  ce0nulnc  6185  fce  6189  ce0tb  6239  ncfin  6248  addccan2nclem2  6265  nchoicelem6  6295  nchoicelem11  6300  nchoicelem12  6301  nchoicelem16  6305  nchoicelem17  6306  nchoicelem18  6307  nchoicelem19  6308  elscan  6331