Theorem eleq2i 1153

Description: Inference from equality to equivalence of membership.

Hypothesis

Ref	Expression
eleq1i.1	⊢ A = B

Assertion

Ref	Expression
eleq2i	⊢ (C ∈ A ↔ C ∈ B)

Proof of Theorem eleq2i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ A = B
2		eleq2 1150	. 2 ⊢ (A = B → (C ∈ A ↔ C ∈ B))
3	1, 2	ax-mp 6	1 ⊢ (C ∈ A ↔ C ∈ B)

Syntax hints:   ↔ wb 127   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  eleq12i 1154  eleqtr 1161  cleqabi 1176  cleqabri 1177  hbrab1 1310  hbrab 1311  cleqrabi 1347  elab2g 1418  elrabf 1421  elrabsf 1456  elabs2 1457  dfnul2 1709  elsncg 1825  hbsn 1833  eltp 1834  tpi1 1843  tpi2 1844  tpi3 1845  hbop 1879  exss 1881  elop 1894  elintrab 1977  hbiu1 2012  hbii1 2013  opabid 2099  hbopab1 2112  hbopab2 2113  brabg 2116  elsuci 2289  elsucg 2290  elsuc2g 2291  sucid 2304  suceloni 2314  elxp 2442  optocl 2469  hbco 2508  opelco 2509  elcnv 2514  opelcnvg 2517  brelrn 2559  hbdm 2565  hbres 2577  opelres 2579  dfima2 2604  fnopabg 2745  elfv 2830  hbfv 2837  ndmfvrcl 2849  nfvres 2850  fvopab3 2868  elrnopab 2884  funfvima 2904  tfrlem7 2955  tfrlem8 2956  tfrlem9 2957  tfrlem11 2959  tfr2 2963  hbrdg 2974  rdgsucopabn 2985  tz7.48-1 2994  tz7.48-2 2995  abianfplem 2999  hbopr 3017  hboprab1 3023  hboprab2 3024  eloprabg 3035  elrnoprab 3054  ndmoprg 3057  1st2val 3097  el1o 3115  oawordeulem 3156  ereldm 3222  ecopqsi 3230  0nelqs 3234  ecelqsdm 3235  ectocl 3238  ecoptocl 3239  brecop 3242  brecop2 3243  eceqopreq 3249  th3qlem1 3250  oprec 3254  elmap 3265  brsdom 3286  enssdom 3287  brdom2 3292  map1 3335  pw2en 3348  sbthlem2 3350  brsdom2 3363  xpmapenlem1 3391  xpmapenlem4 3394  inf3lema 3460  trcl 3489  zfregs 3491  r1tr 3498  tz9.12lem1 3503  tz9.12lem3 3505  rankr1 3518  rankel 3524  rankpw 3528  rankss 3531  rankun 3535  r1rankid 3537  aceq3lem 3555  aceq3 3556  aceq5lem2 3559  aceq5lem3 3560  aceq5lem4 3561  aceq5lem5 3562  ac6lem 3575  zornlem2 3604  hta 3619  cardlim 3657  cardsdomel 3658  alephon 3671  alephcard 3673  alephnbtwn 3674  alephnbtwn2 3675  alephord2 3681  alephgeom 3687  cfub 3703  cardcf 3706  cflecard 3707  cfle 3708  cfsuc 3709  elcard 3713  elni 3798  ltpiord 3809  nlt1pi 3827  enqeceq 3841  0npq 3844  addclpq 3852  mulclpq 3854  enreceq 3971  0nsr 3982  addclsr 3986  mulclsr 3987  opelcn 4042  opelreal 4043  elreal 4044  0ncn 4045  addcnsr 4047  mulcnsr 4048  axaddex 4059  axmulex 4060  axaddcl 4066  axmulcl 4068  axnegex 4078  leltt 4278  peano2nn 4433  nnind 4434  elnn0 4536  elz 4565  uzwo3lem2 4615  elq 4629  om2uzsuc 4652  uzrdgval 4657  seqlem1 4662  seqsuclem 4669  sqrlem4 4734  infxpidmlem6 4938  infxpidmlem7 4939  infmap2lem1 4951  elch0 5158  chocuni 5179  projlem8 5200  projlem10 5202  projlem13 5205  projlem15 5207  omlsilem 5249  pjoc1 5268  shslej 5339  shmods 5363  h1de2ctlem 5460  elspansn 5463  spansncv 5542  5oalem1 5544  5oalem2 5545  3oalem2 5553  hoco 5598  pj3lem1 5658  elat 5738

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org