Theorem eleq2 2083

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq2	|- (A = B -> ( C e. A <-> C e. B))

Proof of Theorem eleq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2016	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 113	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1432	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 440	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1688	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 2018	. 2 |- ( C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 2018	. 2 |- ( C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3bitr4g 212	1 |- (A = B -> ( C e. A <-> C e. B))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  A.wal 1226   = wceq 1228  E.wex 1362   e. wcel 1374

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-cleq 2015  df-clel 2018

This theorem is referenced by:  eleq12  2084  eleq2i  2086  eleq2d  2089  nelneq2  2121  clelsb4  2125  dvelimdc  2179  nelne1  2273  neleq2  2280  raleqf  2479  rexeqf  2480  reueq1f  2481  rmoeq1f  2482  rabeqf  2528  clel3g  2655  clel4  2657  sbcel2gv  2799  sbnfc2  2883  difeq2  3033  uneq1  3067  ineq1  3108  n0i  3206  disjel  3251  exsnrex  3387  sneqr  3505  preqr1g  3511  preqr1  3513  preq12b  3515  prel12  3516  elunii  3559  eluniab  3566  ssuni  3576  elinti  3598  elintab  3600  intss1  3604  intmin  3609  intab  3618  iineq2  3648  dfiin2g  3664  breq  3740  axsep2  3850  zfauscl  3851  inuni  3883  rext  3925  intid  3934  mss  3936  opth1  3947  opeqex  3960  limeq  4063  nsuceq0g  4104  suctrALT  4107  snnex  4131  uniuni  4133  iunpw  4161  ordtriexmidlem  4192  ordtriexmidlem2  4193  ordtriexmid  4194  ordtri2orexmid  4195  onsucelsucexmidlem  4198  onsucelsucexmid  4199  ordsucunielexmid  4200  regexmidlem1  4202  regexmid  4203  elirr  4208  en2lp  4216  suc11g  4219  dtruex  4221  ordsoexmid  4224  nlimsucg  4226  onpsssuc  4231  peano5  4248  limom  4263  0elnn  4267  nn0eln0  4268  nnregexmid  4269  xpeq1  4286  xpeq2  4287  opthprc  4318  xp11m  4686  funopg  4860  dffo4  5240  elunirn  5330  f1oiso  5390  eusvobj2  5422  acexmidlema  5427  acexmidlemb  5428  acexmidlemab  5430  acexmidlem2  5433  mpt2eq123  5487  unielxp  5723  cnvf1o  5769  smoel  5837  nnsucelsuc  5985  nntri3or  5987  nntri2  5988  nndceq  5990  nnmordi  6000  nnaordex  6011  elqsn0m  6085  qsel  6094  elni2  6174  addnidpig  6196  elinp  6328  bdsep2  7112  bdzfauscl  7116  bj-indeq  7152  peano5set  7162  bj-nn0suc0  7172  bj-nnelirr  7175  bj-peano4  7177  bj-inf2vnlem2  7189  bj-nn0sucALT  7196  bj-findis  7197