Theorem eleq1d 1540

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 1534	. 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 956   e. wcel 958

This theorem is referenced by:  eleq12d 1542  eqeltrd 1548  hbsbc1gd 1983  hbsbcgd 1984  sbcel2g 2015  sbccsb2g 2023  breq1 2622  breq2 2623  brprc 2661  inex1g 2718  intex 2729  pwex 2745  pwexg 2746  snex 2750  prex 2781  opabsb 2815  uniex 2870  uniexg 2871  unexb 2873  rabxfr 2902  onint 3006  trsuc 3055  limsuc 3120  opelxp1 3205  opelxp 3214  opelxpg 3216  opabid2 3267  opelcog 3290  dfdmf 3306  eldm2g 3309  opeldm 3314  elreldm 3338  dfrnf 3348  elrn2 3349  opelresg 3374  iss 3397  elimasn 3426  elimasng 3427  intirr 3441  cnvopab 3445  xpexr 3479  unielrel 3514  funopg 3547  funimaexg 3575  fnex 3607  fnopabg 3615  fcoi1 3645  fcoi2 3646  fornex 3679  tz6.12f 3738  ndmfvrcl 3746  funopfvg 3752  ssimaex 3768  dmfco 3773  fvco 3774  fvopabn 3786  fvopab5 3793  funfvop 3803  fvelrn 3812  fopab2 3823  ffnfvf 3829  fopabco 3832  fsn 3834  fressnfv 3838  funfvima 3852  funfvima3 3854  abrexexg 3861  tfrlem9 3919  tz7.48-2 3957  abianfp 3962  ffnoprval 4014  foprcl 4015  ndmoprcl 4044  ndmoprrcl 4046  caoprcl 4052  f1stres 4093  f2ndres 4094  unielxp 4107  foprab2 4119  oacl 4170  omcl 4171  oecl 4172  oaord1 4185  omordi 4197  oen0 4213  oeordi 4214  nnacl 4229  nnmcl 4230  nnecl 4231  omsmolem 4256  dfec2 4264  ecelqsi 4292  elixp2 4349  fundmen 4427  mapxpen 4493  xpmapenlem5 4498  unblem2 4536  fiint 4552  abfii2 4554  dfom3 4622  ranklim 4677  r1pw 4678  ranksn 4681  aceq3lem 4724  aceq4 4726  aceq5lem1 4727  aceq5lem5 4731  aceq6a 4733  aceq6b 4734  ac6lem 4746  numthlem 4775  zorn2lem1 4780  brdom7disj 4796  brdom6disj 4797  unidom 4800  alephon 4857  alephfplem3 4890  alephfplem4 4891  addnidpi 5020  indpi 5026  addclpq 5050  mulclpq 5052  addclprlem2 5111  mulclprlem 5113  distrlem4pr 5122  prlem934a 5129  prlem934 5131  ltexprlem3 5136  ltexprlem4 5137  ltexprlem7 5140  ltexpri 5141  prlem936 5147  reclem1pr 5148  reclem2pr 5149  reclem3pr 5150  addclsr 5184  mulclsr 5185  suppsr 5214  suppsr2 5215  supsrlem4 5220  supsr 5223  supre 5252  axaddopr 5257  axmulopr 5258  axaddrcl 5264  axmulrcl 5266  pre-axsup 5283  subclt 5359  renegclt 5429  divclz 5699  divclt 5700  redivclz 5787  redivclt 5788  peano2nn 5923  nnaddclt 5928  nnmulclt 5929  nnsub 5944  nnsubt 5945  nndivtrt 5948  infm3 6042  infmsup 6056  infmrcl 6057  nn0mulclt 6111  nnnn0addclt 6113  elz 6125  nnnegz 6126  nn0subt 6149  zaddclt 6153  elnnnn0 6160  zmulclt 6168  nneo 6185  nneot 6186  zeot 6187  zneo 6188  dfuz 6190  om2uzuz 6283  seq1rn2 6307  ser1recl 6317  shftf 6337  uzaddclt 6435  fzrev2t 6498  fsequb 6509  seqzrn2 6542  ser0cl1 6550  expcllem 6561  sqrlem21 6679  sqrcl 6686  sqrclt 6696  sqr2irrlem2 6711  crulem 6722  cjmulrclt 6786  facclt 6925  facdivt 6927  facndivt 6928  bccl2t 6956  clim 6962  fsum1 6990  fsumcllem 6999  csbfsum 7012  ser1ser0 7033  serzcl2t 7034  serzrelem 7046  clmnns 7069  climshft 7089  climres 7090  iserzshft2 7092  climrecl 7095  climge0 7097  climaddlem1 7099  climmullem6 7110  clim2serz 7130  climabslem 7133  serzf0 7154  isum1p 7191  isumnn0nna 7193  isumclt 7194  iserzgt0 7196  isummulc1ALT 7198  isummulc1a 7199  isumcmpi 7200  infcvgaux2 7205  infcvglem3 7208  negfcncf 7254  dsupivthlem 7276  reefclt 7303  absef01tlub 7373  znnen 7487  infpnlem2 7492  infpn2 7494  ruclem13 7507  ruclem33 7527  ruclem35 7529  uniopnt 7583  inopnt 7585  tpsex 7590  iscld 7654  isopn2 7658  islp2 7732  iscn 7743  cnpval 7744  iscnp 7745  cnima 7752  iscncl 7755  cnclima 7756  cncnplem4 7762  methaus 7867  lmbr 7913  iscau 7921  iscau3 7923  iscau4 7925  lmfexlem2 7942  lmle 7945  fsumcnlem 7974  iscms2lem4 7977  lmcau 7981  ghgrpilem4 8121  vcoprne 8183  vcex 8184  nvvcop 8198  nvvop 8213  isnvlem 8214  nvex 8215  nvi 8218  imsmet 8309  ipfval 8337  nmorepnf 8416  phpar 8468  siilem2 8497  isbn 8509  spwnex3 8640  sincolem 8650  eff1i 8729  effoi 8730  pilog 8753  shaddclt 9070  shaddcltOLD 9071  shmulclt 9072  shmulcltOLD 9073  hsn0elch 9105  hhssablt 9118  hhssnvt 9120  hhsssh 9124  occlt 9167  projlem10 9180  shsclt 9267  shintclt 9279  chintclt 9281  shinclt 9336  chinclt 9407  h1datom 9489  osumlem8 9570  sumspansnt 9579  spansncv 9582  5oalem2 9585  5oalem3 9586  pjin 9629  pjjs 9630  eigpos 9747  nmoprepnf 9779  nmfnrepnf 9792  dmadjrnb 9815  lnophmlem1 9926  lnophmt 9929  nmcopext 9944  nmbdfnlbt 9964  nmcfnext 9973  leopg 10040  pjbdln 10061  pjhmopt 10062  hmopidmcht 10066  pjclem4 10112  pj3s 10120  strlem1 10162  atssmat 10290  atcv0eq 10291  atcv1t 10292  atoml 10294  atcvatlem 10297  cdj3lem2a 10348  cdj3lem3a 10351  ghomgrpilem2 10371  ghomgrplem 10374  symggrp 10393  cayleylem2 10395  fveleq 10400  findreccl 10402  findabrcl 10403  nndivsub 10406  mapudiscn 10484  ishomeo 10489  cmphmp 10493  cnvhmpha 10497  cnvhmphb 10498  cnvhmph 10499  hmphsyma 10500  hmphre 10502  homcard 10511  qusp 10515  fgsb 10529  filint2 10531  fgsb2 10535  isded 10612  dedi 10613  1ded 10614  cmppfd 10621  iscat 10630  cati 10631

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-cleq 1469  df-clel 1472

Copyright terms: Public domain