Theorem eleq2 2241

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 2171	. . . . . 6 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
2	1	biimpi 120	. . . . 5 |- ( A = B -> A. x ( x e. A <-> x e. B ) )
3	2	19.21bi 1558	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 464	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1825	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2173	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2173	. 2 |- ( C e. B <-> E. x ( x = C /\ x e. B ) )
8	5, 6, 7	3bitr4g 223	1 |- ( A = B -> ( C e. A <-> C e. B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1351   = wceq 1353   E.wex 1492   e. wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12  2242  eleq2i  2244  eleq2d  2247  nelneq2  2279  clelsb2  2283  dvelimdc  2340  nelne1  2437  neleq2  2447  raleqf  2668  rexeqf  2669  reueq1f  2670  rmoeq1f  2671  rabeqf  2727  clel3g  2871  clel4  2873  sbcbi2  3013  sbcel2gv  3026  csbeq2  3081  sbnfc2  3117  difeq2  3247  uneq1  3282  ineq1  3329  nel02  3427  n0i  3428  disjel  3477  exsnrex  3634  sneqr  3760  preqr1g  3766  preqr1  3768  preq12b  3770  prel12  3771  elunii  3814  eluniab  3821  ssuni  3831  elinti  3853  elintab  3855  intss1  3859  intmin  3864  intab  3873  iineq2  3903  dfiin2g  3919  breq  4005  axsep2  4122  zfauscl  4123  inuni  4155  exmidexmid  4196  ss1o0el1  4197  exmid01  4198  exmidundif  4206  exmidundifim  4207  rext  4215  intid  4224  mss  4226  opth1  4236  opeqex  4249  frforeq3  4347  frirrg  4350  limeq  4377  nsuceq0g  4418  suctr  4421  snnex  4448  uniuni  4451  iunpw  4480  ordtriexmidlem  4518  ordtriexmidlem2  4519  ordtriexmid  4520  ontriexmidim  4521  ordtri2orexmid  4522  ontr2exmid  4524  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  onsucelsucexmid  4529  ordsucunielexmid  4530  regexmidlem1  4532  reg2exmidlema  4533  regexmid  4534  reg2exmid  4535  elirr  4540  en2lp  4553  suc11g  4556  dtruex  4558  ordsoexmid  4561  nlimsucg  4565  onintexmid  4572  reg3exmidlemwe  4578  reg3exmid  4579  peano5  4597  limom  4613  0elnn  4618  nn0eln0  4619  nnregexmid  4620  xpeq1  4640  xpeq2  4641  opthprc  4677  xp11m  5067  funopg  5250  dffo4  5664  elunirn  5766  f1oiso  5826  canth  5828  eusvobj2  5860  acexmidlema  5865  acexmidlemb  5866  acexmidlemab  5868  acexmidlem2  5871  mpoeq123  5933  oprssdmm  6171  unielxp  6174  cnvf1o  6225  smoel  6300  tfr0dm  6322  frecabcl  6399  nnsucelsuc  6491  nntri3or  6493  nntri2  6494  nntri3  6497  nndceq  6499  nnmordi  6516  nnaordex  6528  elqsn0m  6602  qsel  6611  mapsn  6689  findcard2s  6889  undifdcss  6921  ctssdclemr  7110  nnnninf2  7124  exmidonfinlem  7191  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  exmidontriimlem3  7221  exmidontriimlem4  7222  exmidontriim  7223  pw1ne3  7228  sucpw1ne3  7230  sucpw1nel3  7231  onntri35  7235  elni2  7312  addnidpig  7334  elinp  7472  suplocexprlemdisj  7718  suplocexprlemub  7721  pitonn  7846  peano1nnnn  7850  peano2nnnn  7851  peano5nnnn  7890  sup3exmid  8913  peano5nni  8921  1nn  8929  peano2nn  8930  dfuzi  9362  uz11  9549  elfzonlteqm1  10209  frec2uzltd  10402  0tonninf  10438  1tonninf  10439  sumeq1  11362  prodeq1f  11559  ctiunct  12440  ssomct  12445  issubm  12862  isnsg  13060  releqgg  13078  issubrg  13340  istopg  13469  fiinbas  13519  topbas  13537  epttop  13560  restbasg  13638  icnpimaex  13681  lmcvg  13687  iscnp4  13688  cncnpi  13698  cnconst2  13703  cnptoprest  13709  cnptoprest2  13710  cnpdis  13712  lmss  13716  lmff  13719  txbas  13728  eltx  13729  txcnp  13741  txlm  13749  blssps  13897  blss  13898  blssexps  13899  blssex  13900  neibl  13961  metss  13964  metrest  13976  xmettx  13980  metcnp3  13981  tgioo  14016  tgqioo  14017  bdsep2  14608  bdzfauscl  14612  bj-indeq  14651  bj-nn0suc0  14672  bj-nnelirr  14675  bj-peano4  14677  bj-inf2vnlem2  14693  bj-nn0sucALT  14700  bj-findis  14701  strcollnft  14706  sscoll2  14710  nninfsellemdc  14729  nninfsellemqall  14734