Theorem eleq1d 1577

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 1571	. 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 144   = wceq 988   e. wcel 990

This theorem is referenced by:  eleq12d 1579  eqeltrd 1585  hbsbc1gd 2023  hbsbcgd 2024  sbcel2g 2058  sbccsb2g 2066  breq1 2672  breq2 2673  brprc 2711  inex1g 2769  intex 2780  pwex 2797  pwexg 2798  snex 2802  prex 2834  opelopabsb 2868  uniex 2924  uniexg 2925  unexb 2927  rabxfr 2957  onint 3061  trsuc 3110  limsuc 3175  opelxp1 3262  opelxp 3271  opelxpg 3273  opabid2 3333  opelco2g 3353  dfdmf 3370  eldm2g 3373  opeldm 3378  elreldm 3398  dfrnf 3408  elrn2 3409  opelresg 3434  iss 3458  elimasn 3489  elimasng 3490  intirr 3504  cnvopab 3508  xpexr 3535  unielrel 3589  funopg 3622  funimaexg 3650  fnex 3682  fnopabg 3690  fcoi1 3720  fcoi2 3721  fornex 3755  tz6.12f 3814  ndmfvrcl 3822  funopfvg 3828  ssimaex 3844  dmfco 3849  fvco 3850  fvopabn 3862  fvopab5 3869  funfvop 3879  fvelrn 3888  fopab2 3899  ffnfvf 3905  fopabco 3908  fsn 3910  fressnfv 3914  funfvima 3928  funfvima3 3930  abrexexg 3937  tfrlem9 3995  tz7.48-2 4033  abianfp 4038  ffnoprval 4091  foprcl 4092  ndmoprcl 4122  ndmoprrcl 4124  caoprcl 4130  f1stres 4171  f2ndres 4172  unielxp 4184  foprab2 4199  oacl 4254  omcl 4255  oecl 4256  oaord1 4269  omordi 4281  oen0 4297  oeordi 4298  nnacl 4313  nnmcl 4314  nnecl 4315  omsmolem 4340  dfec2 4348  ecelqsi 4379  elixp2 4436  fundmen 4515  mapxpen 4584  xpmapenlem5 4589  unblem2 4628  unifi 4642  fiint 4644  abfii2 4646  iunfi 4653  pwfi 4655  dfom3 4716  ranklim 4771  r1pw 4772  ranksn 4775  aceq3lem 4818  aceq4 4820  aceq5lem1 4821  aceq5lem5 4825  aceq6a 4827  aceq6b 4828  ac6lem 4840  numthlem 4869  zorn2lem1 4874  brdom7disj 4890  brdom6disj 4891  unidom 4894  alephon 4954  alephfplem3 4987  alephfplem4 4988  addnidpi 5117  indpi 5123  addclpq 5147  mulclpq 5149  addclprlem2 5208  mulclprlem 5210  distrlem4pr 5219  prlem934a 5226  prlem934 5228  ltexprlem3 5233  ltexprlem4 5234  ltexprlem7 5237  ltexpri 5238  prlem936 5244  reclem1pr 5245  reclem2pr 5246  reclem3pr 5247  addclsr 5281  mulclsr 5282  suppsr 5311  suppsr2 5312  supsrlem4 5317  supsr 5320  supre 5349  axaddopr 5354  axmulopr 5355  axaddrcl 5361  axmulrcl 5363  pre-axsup 5380  subcl 5456  renegcl 5526  divclzi 5800  divcl 5801  redivclzi 5883  redivcl 5884  peano2nn 6022  nnaddcl 6027  nnmulcl 6028  nnsubi 6044  nnsub 6045  nndivtr 6048  infm3 6164  infmsup 6178  infmrcl 6179  nn0mulcl 6233  nnnn0addcl 6235  elz 6247  nnnegz 6248  nn0sub 6271  zaddcl 6275  elnnnn0 6282  zmulcl 6290  nneoi 6310  nneo 6311  zeo 6312  zneo 6313  dfuzi 6315  irradd 6357  irrmul 6358  uzaddcl 6509  fzrev2 6572  fsequb 6583  om2uzuzi 6589  seq1rn2 6614  ser1recli 6624  shftf 6644  seqzrn2 6679  ser0cl1i 6687  expcllem 6698  sqrlem21 6816  sqrcli 6823  sqrcl 6833  sqr2irrlem2 6848  crulem 6859  cjmulrcl 6924  faccl 7063  facdiv 7065  facndiv 7066  bccl2 7094  clim 7100  fsum1i 7128  fsumcllem 7137  csbfsum 7150  ser1ser0i 7171  serzcl2 7172  serzrelem 7184  clmnnsi 7207  climshfti 7227  climresi 7228  iserzshft2i 7230  climrecl 7233  climge0 7235  climaddlem1 7237  climmullem6 7248  clim2serzi 7268  climabslem 7271  serzf0i 7292  isum1p 7329  isumnn0nnai 7331  isumcl 7332  iserzgt0 7334  isummulc1iALT 7336  isummulc1ai 7337  isumcmpii 7338  infcvgaux2i 7343  infcvglem3 7346  negfcncfi 7392  dsupivthlem 7414  reefcl 7441  absef01tlubi 7511  znnen 7627  infpnlem2 7632  infpn2 7634  ruclem13 7647  ruclem33 7667  ruclem35 7669  uniopn 7723  inopn 7725  tpsex 7730  iscld 7789  isopn2 7793  islp2 7867  iscn 7878  cnpval 7879  iscnp 7880  cnima 7887  iscncl 7890  cnclima 7891  cncnplem4 7897  methaus 8002  lmbr 8048  iscau 8056  iscau3 8058  iscau4 8060  lmfexlem2 8077  lmle 8080  fsumcnlem 8109  iscms2lem4 8112  lmcau 8116  ghgrpilem4 8255  vcoprne 8317  vcex 8318  nvvcop 8332  nvvop 8347  isnvlem 8348  nvex 8349  nvi 8352  imsmet 8443  ipfval 8471  nmorepnf 8550  phpar 8602  siilem2 8631  isbn 8643  spwnex3 8774  sincolem 8783  eff1i 8863  effoi 8864  pilog 8887  shaddcl 9205  shaddclOLD 9206  shmulcl 9207  shmulclOLD 9208  hsn0elch 9240  hhssabl 9253  hhssnvt 9255  hhsssh 9259  occl 9302  projlem10 9315  shscl 9402  shintcl 9414  chintcl 9416  shincl 9471  chincl 9542  h1datomi 9624  osumlem8 9705  sumspansn 9714  spansncvi 9717  5oalem2 9720  5oalem3 9721  pjini 9764  pjjsi 9765  eigposi 9882  nmoprepnf 9912  nmfnrepnf 9925  dmadjrnb 9948  lnophmlem1 10058  lnophm 10061  nmcopex 10076  nmbdfnlb 10096  nmcfnex 10105  leopg 10172  pjbdlni 10193  pjhmop 10194  hmopidmch 10198  pjclem4 10245  pj3si 10253  strlem1 10295  atssma 10423  atcv0eq 10424  atcv1 10425  atomli 10427  atcvatlem 10430  cdj3lem2a 10481  cdj3lem3a 10484  ghomgrpilem2 10507  ghomgrplem 10510  symggrp 10529  cayleylem2 10531  fveleq 10538  findreccl 10540  findabrcl 10541  nndivsub 10544  ref3w 10603  mapudiscn 10648  ishomeo 10653  cmphmp 10657  cnvhmpha 10661  cnvhmphb 10662  cnvhmph 10663  hmphsyma 10664  hmphre 10666  homcard 10675  hmeobc 10678  homindlem3 10687  qusp 10694  filint 10701  fgsb 10708  filint2 10710  fgsb2 10713  isded 10804  dedi 10805  1ded 10806  cmppfd 10813  iscat 10822  cati 10823

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-17 1003  ax-4 1005  ax-5o 1007  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-cleq 1505  df-clel 1508

Copyright terms: Public domain