Theorem eleq1d 1537

Description: Deduction from equality to equivalence of membership.

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 1531	. 2 |- (A = B -> (A e. C <-> B e. C))
3	1, 2	syl 10	1 |- (ph -> (A e. C <-> B e. C))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956

This theorem is referenced by:  eleq12d 1539  eqeltrd 1545  hbsbc1gd 1979  hbsbcgd 1980  sbcel2g 2011  sbccsb2g 2019  breq1 2617  breq2 2618  brprc 2656  inex1g 2713  intex 2724  pwex 2740  pwexg 2741  snex 2745  prex 2776  opabsb 2810  uniex 2865  uniexg 2866  unexb 2868  rabxfr 2897  onint 3001  trsuc 3050  limsuc 3115  opelxp1 3200  opelxp 3209  opelxpg 3211  opabid2 3262  opelcog 3285  dfdmf 3301  eldm2g 3304  opeldm 3309  elreldm 3333  dfrnf 3342  elrn2 3343  opelresg 3366  iss 3389  elimasn 3418  elimasng 3419  intirr 3433  cnvopab 3437  xpexr 3471  unielrel 3506  funopg 3539  funimaexg 3567  fnex 3599  fnopabg 3607  fcoi1 3636  fcoi2 3637  fornex 3670  tz6.12f 3729  ndmfvrcl 3737  funopfvg 3743  ssimaex 3759  dmfco 3764  fvco 3765  fvopabn 3777  fvopab5 3784  funfvop 3794  fvelrn 3803  fopab2 3814  ffnfvf 3820  fopabco 3823  fsn 3825  fressnfv 3829  funfvima 3843  funfvima3 3845  abrexexg 3852  tfrlem9 3910  tz7.48-2 3948  abianfp 3953  ffnoprval 4005  foprcl 4006  ndmoprcl 4036  ndmoprrcl 4038  caoprcl 4044  f1stres 4083  f2ndres 4084  unielxp 4097  foprab2 4109  oacl 4160  omcl 4161  oecl 4162  oaord1 4175  omordi 4187  oen0 4203  oeordi 4204  nnacl 4219  nnmcl 4220  nnecl 4221  omsmolem 4246  dfec2 4254  ecelqsi 4282  elixp2 4339  fundmen 4415  mapxpen 4481  xpmapenlem5 4486  unblem2 4524  fiint 4540  abfii2 4542  dfom3 4610  ranklim 4665  r1pw 4666  ranksn 4669  aceq3lem 4712  aceq4 4714  aceq5lem1 4715  aceq5lem5 4719  aceq6a 4721  aceq6b 4722  ac6lem 4734  numthlem 4763  zorn2lem1 4768  brdom7disj 4784  brdom6disj 4785  unidom 4788  alephon 4845  alephfplem3 4878  alephfplem4 4879  addnidpi 5008  indpi 5014  addclpq 5038  mulclpq 5040  addclprlem2 5099  mulclprlem 5101  distrlem4pr 5110  prlem934a 5117  prlem934 5119  ltexprlem3 5124  ltexprlem4 5125  ltexprlem7 5128  ltexpri 5129  prlem936 5135  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  addclsr 5172  mulclsr 5173  suppsr 5202  suppsr2 5203  supsrlem4 5208  supsr 5211  supre 5240  axaddopr 5245  axmulopr 5246  axaddrcl 5252  axmulrcl 5254  pre-axsup 5271  subclt 5347  renegclt 5417  divclz 5688  divclt 5689  redivclz 5763  redivclt 5764  peano2nn 5891  nnaddclt 5896  nnmulclt 5897  nnsub 5911  nnsubt 5912  nndivtrt 5915  infm3 6009  infmsup 6023  infmrcl 6024  nn0mulclt 6078  nnnn0addclt 6080  elz 6092  nnnegz 6093  nn0subt 6116  zaddclt 6120  elnnnn0 6127  zmulclt 6135  nneo 6152  nneot 6153  zeot 6154  zneo 6155  zneoOLD 6156  dfuz 6158  om2uzuz 6242  seq1rn2 6266  ser1recl 6276  shftf 6296  uzaddclt 6389  fzrev2t 6452  fsequb 6463  seqzrn2 6496  ser0cl1 6504  expcllem 6515  sqrlem21 6631  sqrcl 6638  sqrclt 6648  sqr2irrlem2 6663  crulem 6674  cjmulrclt 6744  facclt 6885  facdivt 6887  facndivt 6888  bccl2t 6917  clim 6923  fsum1 6951  fsumcllem 6960  csbfsum 6973  ser1ser0 6994  serzcl2t 6995  serzrelem 7007  clmnns 7030  climshft 7049  climres 7050  iserzshft2 7052  climrecl 7055  climge0 7057  climaddlem1 7058  climmullem6 7069  clim2serz 7089  climabslem 7092  serzf0 7113  isum1p 7149  isumnn0nna 7151  isumclt 7152  iserzgt0 7154  isummulc1ALT 7156  isummulc1a 7157  isumcmpi 7158  infcvgaux2 7163  infcvglem3 7166  negfcncf 7212  dsupivthlem 7234  ivth2OLD 7242  reefclt 7268  absef01tlub 7337  znnen 7453  infpnlem2 7458  infpn2 7460  ruclem13 7473  ruclem33 7493  ruclem35 7495  uniopnt 7548  inopnt 7550  tpsex 7555  iscld 7619  isopn2 7623  islp2 7697  iscn 7708  cnpval 7709  iscnp 7710  cnima 7717  iscncl 7720  cnclima 7721  cncnplem4 7727  methaus 7834  lmbr 7880  iscau 7888  iscau3 7890  iscau4 7892  lmfexlem2 7908  lmle 7911  fsumcnlem 7939  iscms2lem4 7942  lmcau 7946  ghgrpilem4 8088  vcoprne 8150  vcex 8151  nvvcop 8165  nvvop 8180  isnvlem 8181  nvex 8182  nvi 8185  imsmet 8275  ipfval 8299  nmorepnf 8376  phpar 8427  siilem2 8456  isbn 8468  spwnex3 8597  sincolem 8603  eff1i 8683  effoi 8684  pilog 8707  shaddclt 9024  shaddcltOLD 9025  shmulclt 9026  shmulcltOLD 9027  hsn0elch 9059  hhssablt 9072  hhssnvt 9074  hhsssh 9078  occlt 9121  projlem10 9134  shsclt 9220  shintclt 9232  chintclt 9234  shinclt 9289  chinclt 9360  h1datom 9444  osumlem8 9525  sumspansnt 9534  spansncv 9537  5oalem2 9540  5oalem3 9541  pjin 9584  pjjs 9585  eigpos 9702  nmoprepnf 9734  nmfnrepnf 9747  dmadjrnb 9770  lnophmlem1 9879  lnophmt 9882  nmcopext 9897  nmbdfnlbt 9917  nmcfnext 9926  leopg 9993  pjbdln 10014  pjhmopt 10015  hmopidmcht 10019  pjclem4 10065  pj3s 10073  strlem1 10115  atssmat 10242  atcv0eq 10243  atcv1t 10244  atoml 10246  atcvatlem 10249  cdj3lem2a 10297  cdj3lem3a 10300  ghomgrpilem2 10320  ghomgrplem 10323  symggrp 10342  cayleylem2 10344  fveleq 10349  findreccl 10351  findabrcl 10352  nndivsub 10357  mapudiscn 10435  ishomeo 10440  cmphmp 10444  cnvhmpha 10448  cnvhmphb 10449  cnvhmph 10450  hmphsyma 10451  hmphre 10453  homcard 10462  qusp 10466  fgsb 10480  filint2 10482  fgsb2 10485  isded 10549  dedi 10550  1ded 10551  cmppfd 10558  iscat 10567  cati 10568

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-cleq 1467  df-clel 1470

Copyright terms: Public domain