Theorem eleq2 2098

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 2031	. . . . . 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 1447	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	anbi2d 437	. . 3 |- (A = B -> ((x = C /\ x e. A) <-> (x = C /\ x e. B)))
5	4	exbidv 1703	. 2 |- (A = B -> (E.x(x = C /\ x e. A) <-> E.x(x = C /\ x e. B)))
6		df-clel 2033	. 2 |- ( C e. A <-> E.x(x = C /\ x e. A))
7		df-clel 2033	. 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 1240   = wceq 1242  E.wex 1378   e. wcel 1390

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033

This theorem is referenced by:  eleq12  2099  eleq2i  2101  eleq2d  2104  nelneq2  2136  clelsb4  2140  dvelimdc  2194  nelne1  2289  neleq2  2296  raleqf  2495  rexeqf  2496  reueq1f  2497  rmoeq1f  2498  rabeqf  2544  clel3g  2672  clel4  2674  sbcel2gv  2816  sbnfc2  2900  difeq2  3050  uneq1  3084  ineq1  3125  n0i  3223  disjel  3268  exsnrex  3404  sneqr  3522  preqr1g  3528  preqr1  3530  preq12b  3532  prel12  3533  elunii  3576  eluniab  3583  ssuni  3593  elinti  3615  elintab  3617  intss1  3621  intmin  3626  intab  3635  iineq2  3665  dfiin2g  3681  breq  3757  axsep2  3867  zfauscl  3868  inuni  3900  rext  3942  intid  3951  mss  3953  opth1  3964  opeqex  3977  limeq  4080  nsuceq0g  4121  suctr  4124  snnex  4147  uniuni  4149  iunpw  4177  ordtriexmidlem  4208  ordtriexmidlem2  4209  ordtriexmid  4210  ordtri2orexmid  4211  onsucelsucexmidlem  4214  onsucelsucexmid  4215  ordsucunielexmid  4216  regexmidlem1  4218  regexmid  4219  elirr  4224  en2lp  4232  suc11g  4235  dtruex  4237  ordsoexmid  4240  nlimsucg  4242  onpsssuc  4247  peano5  4264  limom  4279  0elnn  4283  nn0eln0  4284  nnregexmid  4285  xpeq1  4302  xpeq2  4303  opthprc  4334  xp11m  4702  funopg  4877  dffo4  5258  elunirn  5348  f1oiso  5408  eusvobj2  5441  acexmidlema  5446  acexmidlemb  5447  acexmidlemab  5449  acexmidlem2  5452  mpt2eq123  5506  unielxp  5742  cnvf1o  5788  smoel  5856  tfr0  5878  nnsucelsuc  6009  nntri3or  6011  nntri2  6012  nntri3  6014  nndceq  6015  nnmordi  6025  nnaordex  6036  elqsn0m  6110  qsel  6119  elni2  6298  addnidpig  6320  elinp  6456  pitonn  6724  peano5nni  7678  1nn  7686  peano2nn  7687  dfuzi  8104  uz11  8251  elfzonlteqm1  8816  frec2uzltd  8850  bdsep2  9320  bdzfauscl  9324  bj-indeq  9364  peano5set  9374  bj-nn0suc0  9384  bj-nnelirr  9387  bj-peano4  9389  bj-inf2vnlem2  9401  bj-nn0sucALT  9408  bj-findis  9409