Theorem eleq2 2414

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 2347	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 186	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1758	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 684	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1626	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 2349	. 2 |- (C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 2349	. 2 |- (C e. B <-> E.x(x = C /\ x e. B))
8	5, 6, 7	3bitr4g 279	1 |- (A = B -> (C e. A <-> C e. B))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. 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:  eleq12  2415  eleq2i  2417  eleq2d  2420  nelneq2  2452  clelsb2  2456  dvelimdc  2510  nelne1  2606  neleq2  2609  raleqf  2804  rexeqf  2805  reueq1f  2806  rmoeq1f  2807  rabeqf  2853  clel3g  2977  clel4  2979  sbcel2gv  3107  sbnfc2  3197  nineq1  3235  uneq1  3412  ineq1  3451  unineq  3506  n0i  3556  disjel  3598  elif  3697  sneqr  3873  unsneqsn  3888  elunii  3897  eluniab  3904  ssuni  3914  elinti  3936  elintab  3938  intss1  3942  intmin  3947  intab  3957  iineq2  3987  dfiin2g  4001  preqr1  4125  preq12b  4128  opkth1g  4131  eluni1g  4173  cnvkeq  4216  ins2keq  4219  ins3keq  4220  imakeq1  4225  sikeq  4242  unipw1  4326  eqpw1uni  4331  pw1eqadj  4333  dfnnc2  4396  0cnsuc  4402  peano5  4410  0fin  4424  nnsucelr  4429  nndisjeq  4430  snfi  4432  ssfin  4471  vfinnc  4472  ncfinprop  4475  ncfineleq  4478  ncfinraise  4482  ncfinlower  4484  nnpw1ex  4485  tfinprop  4490  nnadjoin  4521  nnpweq  4524  sfineq1  4527  sfineq2  4528  sfinltfin  4536  spfininduct  4541  vfin1cltv  4548  vfinspsslem1  4551  phi11lem1  4596  phi011lem1  4599  proj1op  4601  proj2op  4602  breq  4642  epelc  4766  xpeq1  4799  xpeq2  4800  fnasrn  5418  f1oiso  5500  ndmovg  5614  mpt2eq123  5662  clos1basesucg  5885  erth  5969  elqsn0  5994  eqncg  6127  ncseqnc  6129  peano4nc  6151  2p1e3c  6157  nntccl  6171  ovce  6173  dflec3  6222  ncfin  6248  addcdi  6251  ncvsq  6257  0lt1c  6259  nmembers1lem1  6269