Theorem eleq2i 2417

Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)

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 2414	. 2 ⊢ (A = B → (C ∈ A ↔ C ∈ B))
3	1, 2	ax-mp 5	1 ⊢ (C ∈ A ↔ C ∈ B)

Syntax hints:   ↔ wb 176   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  eleq12i  2418  eleqtri  2425  eleq2s  2445  hbxfreq  2456  abeq2i  2460  abeq1i  2461  nfceqi  2485  raleqbii  2644  rexeqbii  2645  rabeq2i  2856  elab2g  2987  elrabf  2993  elrab2  2996  cbvsbc  3074  elcomplg  3218  elin  3219  elun  3220  eldif  3221  elsymdif  3223  elin2  3446  dfnul2  3552  noel  3554  eltpg  3769  tpid3g  3831  elunirab  3904  elintrab  3938  elopk  4129  elpw1  4144  eluni1g  4172  opkelcokg  4261  opkelimagekg  4271  cokrelk  4284  peano1  4402  peano2  4403  elfin  4420  el0c  4421  nnsucelr  4428  nndisjeq  4429  ssfin  4470  eqtfinrelk  4486  nnadjoin  4520  spfinsfincl  4539  proj1op  4600  proj2op  4601  eqop  4611  brabsb  4698  brabga  4701  el1st  4729  elswap  4740  dfswap2  4741  elxp  4801  elcnv  4889  elrn  4896  eldm  4898  elima1c  4947  brelrn  4960  elimasn  5019  rninxp  5060  elfv  5326  nfvres  5352  fv01  5354  fvopab3g  5386  f0cli  5418  funfvima  5459  elunirn  5470  eloprabga  5578  ovidig  5593  ndmovcl  5614  ndmov  5615  fvmptex  5721  elfix  5787  otelins2  5791  otelins3  5792  oqelins4  5794  otsnelsi3  5805  composeex  5820  clos1conn  5879  clos1basesucg  5884  elec  5964  elncs  6119  elnc  6125  el2c  6191  tcfnex  6244  csucex  6259  nchoicelem10  6298  nchoicelem18  6306