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  dvelimdc  2509  nelne1  2605  neleq2  2608  raleqf  2803  rexeqf  2804  reueq1f  2805  rmoeq1f  2806  rabeqf  2852  clel3g  2976  clel4  2978  sbcel2gv  3106  sbnfc2  3196  nineq1  3234  uneq1  3411  ineq1  3450  unineq  3505  n0i  3555  disjel  3597  elif  3696  sneqr  3872  unsneqsn  3887  elunii  3896  eluniab  3903  ssuni  3913  elinti  3935  elintab  3937  intss1  3941  intmin  3946  intab  3956  iineq2  3986  dfiin2g  4000  preqr1  4124  preq12b  4127  opkth1g  4130  eluni1g  4172  cnvkeq  4215  ins2keq  4218  ins3keq  4219  imakeq1  4224  sikeq  4241  unipw1  4325  eqpw1uni  4330  pw1eqadj  4332  dfnnc2  4395  0cnsuc  4401  peano5  4409  0fin  4423  nnsucelr  4428  nndisjeq  4429  snfi  4431  ssfin  4470  vfinnc  4471  ncfinprop  4474  ncfineleq  4477  ncfinraise  4481  ncfinlower  4483  nnpw1ex  4484  tfinprop  4489  nnadjoin  4520  nnpweq  4523  sfineq1  4526  sfineq2  4527  sfinltfin  4535  spfininduct  4540  vfin1cltv  4547  vfinspsslem1  4550  phi11lem1  4595  phi011lem1  4598  proj1op  4600  proj2op  4601  breq  4641  epelc  4765  xpeq1  4798  xpeq2  4799  fnasrn  5417  f1oiso  5499  ndmovg  5613  mpt2eq123  5661  clos1basesucg  5884  erth  5968  elqsn0  5993  eqncg  6126  ncseqnc  6128  peano4nc  6150  2p1e3c  6156  nntccl  6170  ovce  6172  dflec3  6221  ncfin  6247  addcdi  6250  ncvsq  6256  0lt1c  6258  nmembers1lem1  6268