Theorem eleq1d 1583

Description: Deduction from equality to equivalence of membership.

Hypothesis

Ref	Expression
eleq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eleq1d	⊢ (φ → (A ∈ C ↔ B ∈ C))

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (φ → A = B)
2		eleq1 1577	. 2 ⊢ (A = B → (A ∈ C ↔ B ∈ C))
3	1, 2	syl 10	1 ⊢ (φ → (A ∈ C ↔ B ∈ C))

Syntax hints:   → wi 3   ↔ wb 144   = wceq 992   ∈ wcel 994

This theorem is referenced by:  eleq12d 1585  eqeltrd 1591  hbsbc1gd 2031  hbsbcgd 2032  sbcel2g 2066  sbccsb2g 2074  breq1 2695  breq2 2696  brprc 2734  inex1g 2792  intex 2803  pwex 2823  pwexg 2824  snex 2826  prex 2857  opelopabsb 2892  trsuc 3056  uniex 3093  uniexg 3094  unexb 3096  rabxfr 3125  onint 3152  limsuc 3203  opelxp1 3288  opelxp 3297  opelxpg 3299  opabid2 3360  opelco2g 3380  dfdmf 3397  eldm2g 3400  opeldm 3405  elreldm 3425  dfrnf 3435  elrn2 3436  opelresg 3461  iss 3487  elimasn 3518  elimasng 3519  intirr 3533  cnvopab 3537  xpexr 3564  unielrel 3619  funopg 3652  funimaexg 3681  fnex 3713  fnopabg 3722  fcoi1 3752  fcoi2 3753  fornex 3787  tz6.12f 3849  ndmfvrcl 3857  funopfvg 3863  ssimaex 3879  dmfco 3884  fvco 3885  fvopabn 3897  fvopab5 3904  funfvop 3917  fvelrn 3926  fopab2 3937  ffnfvf 3943  fopabco 3946  fsn 3948  fressnfv 3952  funfvima 3966  funfvima3 3968  abrexexg 3975  ffnoprv 4074  foprcl 4075  ndmoprcl 4105  ndmoprrcl 4107  caoprcl 4113  f1stres 4154  f2ndres 4155  unielxp 4167  foprab2 4181  tfrlem9 4220  tz7.48-2 4258  abianfp 4263  oacl 4306  omcl 4307  oecl 4308  oaord1 4321  omordi 4333  oen0 4349  oeordi 4350  nnacl 4369  nnmcl 4370  nnecl 4371  omsmolem 4396  dfec2 4404  ecelqsi 4432  elixp2 4490  fundmen 4569  mapxpen 4642  xpmapenlem5 4647  xpfi 4685  unblem2 4687  unifi 4701  fiint 4703  abfii2 4705  iunfi 4712  pwfi 4714  dfom3 4776  ranklim 4831  r1pw 4832  ranksn 4835  aceq3lem 4878  aceq4 4880  aceq5lem1 4881  aceq5lem5 4885  aceq6a 4887  aceq6b 4888  ac6lem 4900  numthlem 4929  zorn2lem1 4934  brdom7disj 4950  brdom6disj 4951  unidom 4954  alephon 5015  alephfplem3 5048  alephfplem4 5049  addnidpi 5182  indpi 5188  addclpq 5212  mulclpq 5214  addclprlem2 5273  mulclprlem 5275  distrlem4pr 5284  prlem934a 5291  prlem934 5293  ltexprlem3 5298  ltexprlem4 5299  ltexprlem7 5302  ltexpri 5303  prlem936 5309  reclem1pr 5310  reclem2pr 5311  reclem3pr 5312  addclsr 5346  mulclsr 5347  suppsr 5376  suppsr2 5377  supsrlem4 5382  supsr 5385  supre 5414  axaddopr 5419  axmulopr 5420  axaddrcl 5426  axmulrcl 5428  pre-axsup 5445  subcl 5521  renegcl 5591  divclzi 5863  divcl 5864  redivclzi 5939  redivcl 5940  peano2nn 6080  nnaddcl 6085  nnmulcl 6086  nnsubi 6102  nnsub 6103  nndivtr 6106  infm3 6222  infmsup 6236  infmrcl 6237  nn0mulcl 6291  nnnn0addcl 6293  elz 6305  nnnegz 6306  nn0sub 6329  zaddcl 6333  elnnnn0 6340  zmulcl 6348  nneoi 6368  nneo 6369  zeo 6370  zneo 6371  dfuzi 6373  zindd 6386  irradd 6416  irrmul 6417  uzaddcl 6576  fzrev2 6643  fsequb 6654  om2uzuzi 6660  seq1rn2 6686  ser1recli 6696  shftf 6716  seqzrn2 6751  ser0cl1i 6759  expcllem 6770  sqrlem21 6894  sqrcli 6901  sqrcl 6911  sqr2irrlem2 6926  crulem 6937  cjmulrcl 7002  faccl 7143  facdiv 7145  facndiv 7146  bccl2 7174  clim 7180  fsum1i 7208  fsumcllem 7217  csbfsum 7230  ser1ser0i 7251  serzcl2 7252  serzrelem 7264  clmnnsi 7287  climshfti 7307  climresi 7308  iserzshft2i 7310  climrecl 7313  climge0 7315  climaddlem1 7317  climmullem6 7328  clim2serzi 7348  climabslem 7351  serzf0i 7372  isum1p 7410  isumnn0nnai 7412  isumcl 7413  iserzgt0 7415  isummulc1iALT 7417  isummulc1ai 7418  isumcmpii 7419  infcvgaux2i 7424  infcvglem3 7427  explecnv 7438  negfcncfi 7474  dsupivthlem 7496  reefcl 7523  absef01tlubi 7593  znnen 7714  infpnlem2 7719  infpn2 7721  ruclem13 7734  ruclem33 7754  ruclem35 7756  uniopn 7810  inopn 7812  tpsex 7817  iscld 7879  isopn2 7883  islp2 7957  iscn 7968  cnpval 7969  iscnp 7970  cnima 7977  iscncl 7980  cnclima 7981  cncnplem4 7987  methaus 8093  lmbr 8139  iscau 8147  iscau3 8149  iscau4 8151  lmfexlem2 8168  lmle 8171  fsumcnlem 8200  iscms2lem4 8203  lmcau 8207  gxcl 8321  gxsuc 8328  ghgrpilem4 8377  drngi 8408  vcoprne 8445  vcex 8446  nvvcop 8460  nvvop 8475  isnvlem 8476  nvex 8477  nvi 8480  imsmet 8571  vacnlem1 8582  vacnlem3 8584  ipfval 8606  nmorepnf 8685  phpar 8739  siilem2 8768  isbn 8781  bnsscmcl 8785  spwnex3 8917  laspwcl 8930  lanfwcl 8931  sincolem 8932  eff1i 9016  effoi 9017  pilog 9040  shaddcl 9361  shaddclOLD 9362  shmulcl 9363  shmulclOLD 9364  hsn0elch 9396  hhssabl 9409  hhssnvt 9411  hhsssh 9415  occl 9458  projlem10 9471  shscl 9558  shintcl 9570  chintcl 9572  shincl 9627  chincl 9698  h1datomi 9780  osumlem8 9863  sumspansn 9872  spansncvi 9875  5oalem2 9878  5oalem3 9879  pjini 9922  pjjsi 9923  eigposi 10042  nmoprepnf 10074  nmfnrepnf 10087  dmadjrnb 10110  lnophmlem1 10220  lnophm 10223  nmcopex 10238  nmbdfnlb 10258  nmcfnex 10267  leopg 10335  pjbdlni 10356  pjhmop 10357  hmopidmch 10361  pjclem4 10408  pj3si 10416  strlem1 10458  atssma 10587  atcv0eq 10588  atcv1 10589  atomli 10591  atcvatlem 10594  cdj3lem2a 10645  cdj3lem3a 10648  ghomgrpilem2 10671  ghomgrplem 10674  symggrp 10693  cayleylem2 10695  fveleq 10700  findreccl 10702  findabrcl 10703  nndivsub 10706  ref3w 10772  prj1 10809  expus 10938  fora2 10953  isdivrng 10968  mapudiscn 11015  ishomeo 11023  cmphmp 11027  cnvhmpha 11031  cnvhmphb 11032  cnvhmph 11033  hmphsyma 11034  hmphre 11036  homcard 11045  hmeobc 11048  homindlem3 11053  stoig 11064  qusp 11068  filint 11075  fgsb 11082  filint2 11084  fgsb2 11086  bwt2 11123  clindistop 11131  bsi2 11139  isded 11190  dedi 11191  1ded 11192  cmppfd 11199  dmrngcmp 11205  iscat 11208  cati 11209  ordtypelem1 11427  hartog 11436  fibas 11452  cnpnei 11472  cncls 11473  cnntr 11474  subcld 11480  cnsubsp2 11484  compsublem 11487  isptfin 11566  islocfin 11567  ptfinfin 11569  finlocfin 11570  locfincomp 11575  locfindsc 11576  neibastop2lem3 11582  topmtcl 11586  ist1-2 11603  t1sncld 11606  isufil2 11650  ufilss 11652  ufileulem 11657  fixufil 11661  ufinffr 11663  cnpfillim 11686  rnelfm 11699  fmfnfmlem2 11701  filnetlem4 11766  filnetlem5 11767  ssga 11777  gapmlem 11783  gapm 11784  respreima 11795  xp1st 11796  xp2nd 11797  oprabco 11811  fixp 11840  inficl 11849  eluzsub 11861  uzp1 11863  fzfi 11864  absz 11868  negmod0 11872  incsequz 11879  iserzshft2 11892  fsumlt1 11894  mettrifi 11912  caures 11917  cnimass 11949  cnres2 11951  cnresima 11952  cnss 11953  cncfres 11956  hmeocnv 11959  hmeoopn 11960  hmeocld 11961  tlmbr 11965  haustlmu 11967  txbas 11973  tx1cn 11976  tx2cn 11977  uptx 11978  txcnopab 11980  txsubsp 11983  heiborlem6 12016  heiborlem16 12026  heiborlem18 12028  heiborlem24 12034  heiborlem28 12038  heiborlem29 12039  heiborlem30 12040  heiborlem32 12042  heiborlem35 12045  phtpycolem5 12097

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514

Copyright terms: Public domain