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  2457  eqabri  2461  eqabcri  2462  nfceqi  2486  raleqbii  2645  rexeqbii  2646  reqabi  2857  elab2g  2988  elrabf  2994  elrab2  2997  cbvsbc  3075  elcomplg  3219  elin  3220  elun  3221  eldif  3222  elsymdif  3224  elin2  3447  dfnul2  3553  noel  3555  eltpg  3770  tpid3g  3832  elunirab  3905  elintrab  3939  elopk  4130  elpw1  4145  eluni1g  4173  opkelcokg  4262  opkelimagekg  4272  cokrelk  4285  peano1  4403  peano2  4404  elfin  4421  el0c  4422  nnsucelr  4429  nndisjeq  4430  ssfin  4471  eqtfinrelk  4487  nnadjoin  4521  spfinsfincl  4540  proj1op  4601  proj2op  4602  eqop  4612  brabsb  4699  brabga  4702  el1st  4730  elswap  4741  dfswap2  4742  elxp  4802  elcnv  4890  elrn  4897  eldm  4899  elima1c  4948  brelrn  4961  elimasn  5020  rninxp  5061  elfv  5327  nfvres  5353  fv01  5355  fvopab3g  5387  f0cli  5419  funfvima  5460  elunirn  5471  eloprabga  5579  ovidig  5594  ndmovcl  5615  ndmov  5616  fvmptex  5722  elfix  5788  otelins2  5792  otelins3  5793  oqelins4  5795  otsnelsi3  5806  composeex  5821  clos1conn  5880  clos1basesucg  5885  elec  5965  elncs  6120  elnc  6126  el2c  6192  tcfnex  6245  csucex  6260  nchoicelem10  6299  nchoicelem18  6307