Theorem eleq1d 1532

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 1526	. 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 953   e. wcel 955

This theorem is referenced by:  eleq12d 1534  eqeltrd 1540  hbsbc1gd 1973  hbsbcgd 1974  sbcel2g 2005  sbccsb2g 2013  breq1 2612  breq2 2613  brprc 2651  inex1g 2708  intex 2719  pwex 2735  pwexg 2736  snex 2740  prex 2771  opabsb 2804  uniex 2861  uniexg 2862  unexb 2864  rabxfr 2892  onint 2996  trsuc 3045  limsuc 3110  opelxp1 3195  opelxp 3204  opelxpg 3206  opabid2 3257  opelcog 3279  dfdmf 3295  eldm2g 3298  opeldm 3303  elreldm 3327  dfrnf 3334  elrn2 3335  opelresg 3358  iss 3381  elimasn 3410  elimasng 3411  intirr 3427  cnvopab 3431  xpexr 3465  unielrel 3500  funopg 3533  funimaexg 3561  fnex 3593  fnopabg 3601  fcoi1 3630  fcoi2 3631  fornex 3664  tz6.12f 3723  ndmfvrcl 3731  funopfvg 3737  ssimaex 3753  dmfco 3758  fvco 3759  fvopabn 3771  fvopab5 3778  funfvop 3788  fvelrn 3797  fopab2 3808  ffnfvf 3814  fopabco 3817  fsn 3819  fressnfv 3823  funfvima 3837  funfvima3 3839  abrexexg 3846  tfrlem9 3904  tz7.48-2 3942  abianfp 3947  ffnoprval 3999  foprcl 4000  ndmoprcl 4030  ndmoprrcl 4032  caoprcl 4038  f1stres 4077  f2ndres 4078  unielxp 4091  foprab2 4103  oacl 4154  omcl 4155  oecl 4156  oaord1 4169  omordi 4181  oen0 4197  oeordi 4198  nnacl 4213  nnmcl 4214  nnecl 4215  omsmolem 4240  dfec2 4248  ecelqsi 4276  elixp2 4333  fundmen 4409  mapxpen 4475  xpmapenlem5 4480  unblem2 4518  fiint 4534  abfii2 4536  dfom3 4602  ranklim 4657  r1pw 4658  ranksn 4661  aceq3lem 4704  aceq4 4706  aceq5lem1 4707  aceq5lem5 4711  aceq6a 4713  aceq6b 4714  ac6lem 4726  numthlem 4755  zorn2lem1 4760  brdom7disj 4776  brdom6disj 4777  unidom 4780  alephon 4837  alephfplem3 4870  alephfplem4 4871  addnidpi 5000  indpi 5006  addclpq 5030  mulclpq 5032  addclprlem2 5091  mulclprlem 5093  distrlem4pr 5102  prlem934a 5109  prlem934 5111  ltexprlem3 5116  ltexprlem4 5117  ltexprlem7 5120  ltexpri 5121  prlem936 5127  reclem1pr 5128  reclem2pr 5129  reclem3pr 5130  addclsr 5164  mulclsr 5165  suppsr 5194  suppsr2 5195  supsrlem4 5200  supsr 5203  supre 5232  axaddopr 5237  axmulopr 5238  axaddrcl 5244  axmulrcl 5246  pre-axsup 5263  subclt 5339  renegclt 5409  divclz 5680  divclt 5681  redivclz 5755  redivclt 5756  peano2nn 5883  nnaddclt 5888  nnmulclt 5889  nnsub 5903  nnsubt 5904  nndivtrt 5907  infm3 6001  infmsup 6015  infmrcl 6016  nn0mulclt 6070  nnnn0addclt 6072  elz 6084  nnnegz 6085  nn0subt 6108  zaddclt 6112  elnnnn0 6119  zmulclt 6127  nneo 6144  nneot 6145  zeot 6146  zneo 6147  zneoOLD 6148  dfuz 6150  om2uzuz 6234  seq1rn2 6258  ser1recl 6268  shftf 6288  uzaddclt 6381  fzrev2t 6444  fsequb 6455  seqzrn2 6488  ser0cl1 6496  expcllem 6507  sqrlem21 6623  sqrcl 6630  sqrclt 6640  sqr2irrlem2 6655  crulem 6666  cjmulrclt 6736  facclt 6877  facdivt 6879  facndivt 6880  bccl2t 6909  clim 6915  fsum1 6943  fsumcllem 6952  csbfsum 6965  ser1ser0 6986  serzcl2t 6987  serzrelem 6999  clmnns 7022  climshft 7041  climres 7042  iserzshft2 7044  climrecl 7047  climge0 7049  climaddlem1 7050  climmullem6 7061  clim2serz 7081  climabslem 7084  serzf0 7105  isum1p 7141  isumnn0nna 7143  isumclt 7144  iserzgt0 7146  isummulc1ALT 7148  isummulc1a 7149  isumcmpi 7150  infcvgaux2 7155  infcvglem3 7158  negfcncf 7204  dsupivthlem 7226  ivth2OLD 7234  reefclt 7260  absef01tlub 7329  znnen 7445  infpnlem2 7450  infpn2 7452  ruclem13 7465  ruclem33 7485  ruclem35 7487  uniopnt 7540  inopnt 7542  tpsex 7547  iscld 7611  isopn2 7615  islp2 7688  iscn 7698  cnpval 7699  iscnp 7700  cnima 7706  iscncl 7709  cnclima 7710  cncnplem4 7716  methaus 7821  lmbr 7866  iscau 7874  iscau3 7876  lmfexlem2 7892  lmle 7895  fsumcnlem 7923  iscms2lem4 7926  lmcau 7930  ghgrpilem4 8073  vcoprne 8136  vcex 8137  nvvcop 8151  nvvop 8166  isnvlem 8167  isnvgOLD 8168  nvex 8169  nvi 8173  imsmet 8262  ipfval 8286  nmorepnf 8363  phpar 8414  siilem2 8443  isbn 8455  spwnex3 8579  sincolem 8584  eff1i 8665  effoi 8666  effoiOLD 8667  pilog 8690  shaddclt 9006  shaddcltOLD 9007  shmulclt 9008  shmulcltOLD 9009  hsn0elch 9041  hhssnvt 9055  hhsssh 9059  occlt 9098  projlem10 9111  shsclt 9197  shintclt 9209  chintclt 9211  shinclt 9266  chinclt 9337  h1datom 9421  osumlem8 9502  sumspansnt 9511  spansncv 9514  5oalem2 9517  5oalem3 9518  pjin 9561  pjjs 9562  eigpos 9679  nmoprepnf 9711  nmfnrepnf 9724  dmadjrnb 9747  lnophmlem1 9856  lnophmt 9859  nmcopext 9874  nmbdfnlbt 9894  nmcfnext 9903  leopg 9967  pjbdln 9987  pjhmopt 9988  hmopidmcht 9992  pjclem4 10037  pj3s 10045  strlem1 10087  atssmat 10213  atcv0eq 10214  atcv1t 10215  atoml 10217  atcvatlem 10220  cdj3lem2a 10268  cdj3lem3a 10271  ghomgrpilem2 10291  ghomgrplem 10294  symggrp 10315  cayleylem2 10317  fveleq 10322  findreccl 10324  findabrcl 10325  mapudiscn 10399  ishomeo 10404  cmphmp 10408  cnvhmpha 10412  cnvhmphb 10413  cnvhmph 10414  hmphsyma 10415  hmphre 10417  homcard 10426  qusp 10430  fgsb 10444  filint2 10446  fgsb2 10449  isded 10513  dedi 10514  1ded 10515  cmppfd 10522  iscat 10531  cati 10532

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain