Theorem eleq2 2253

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 2183	. . . . . 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 1569	. . . 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 1836	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2185	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2185	. 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 1362   = wceq 1364   E.wex 1503   e. wcel 2160

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185

This theorem is referenced by:  eleq12  2254  eleq2i  2256  eleq2d  2259  nelneq2  2291  clelsb2  2295  dvelimdc  2353  nelne1  2450  neleq2  2460  raleqf  2682  rexeqf  2683  reueq1f  2684  rmoeq1f  2685  rabeqf  2742  clel3g  2886  clel4  2888  sbcbi2  3028  sbcel2gv  3041  csbeq2  3096  sbnfc2  3132  difeq2  3262  uneq1  3297  ineq1  3344  nel02  3442  n0i  3443  disjel  3492  exsnrex  3649  sneqr  3775  preqr1g  3781  preqr1  3783  preq12b  3785  prel12  3786  elunii  3829  eluniab  3836  ssuni  3846  elinti  3868  elintab  3870  intss1  3874  intmin  3879  intab  3888  iineq2  3918  dfiin2g  3934  breq  4020  axsep2  4137  zfauscl  4138  inuni  4173  exmidexmid  4214  ss1o0el1  4215  exmid01  4216  exmidundif  4224  exmidundifim  4225  rext  4233  intid  4242  mss  4244  opth1  4254  opeqex  4267  frforeq3  4365  frirrg  4368  limeq  4395  nsuceq0g  4436  suctr  4439  snnex  4466  uniuni  4469  iunpw  4498  ordtriexmidlem  4536  ordtriexmidlem2  4537  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  ontr2exmid  4542  ordtri2or2exmidlem  4543  onsucelsucexmidlem  4546  onsucelsucexmid  4547  ordsucunielexmid  4548  regexmidlem1  4550  reg2exmidlema  4551  regexmid  4552  reg2exmid  4553  elirr  4558  en2lp  4571  suc11g  4574  dtruex  4576  ordsoexmid  4579  nlimsucg  4583  onintexmid  4590  reg3exmidlemwe  4596  reg3exmid  4597  peano5  4615  limom  4631  0elnn  4636  nn0eln0  4637  nnregexmid  4638  xpeq1  4658  xpeq2  4659  opthprc  4695  xp11m  5085  funopg  5269  dffo4  5685  elunirn  5788  f1oiso  5848  canth  5850  eusvobj2  5883  acexmidlema  5888  acexmidlemb  5889  acexmidlemab  5891  acexmidlem2  5894  mpoeq123  5956  oprssdmm  6197  unielxp  6200  cnvf1o  6251  smoel  6326  tfr0dm  6348  frecabcl  6425  nnsucelsuc  6517  nntri3or  6519  nntri2  6520  nntri3  6523  nndceq  6525  nnmordi  6542  nnaordex  6554  elqsn0m  6630  qsel  6639  mapsn  6717  pw2f1odclem  6863  findcard2s  6919  undifdcss  6952  ctssdclemr  7142  nnnninf2  7156  exmidonfinlem  7223  exmidfodomrlemr  7232  exmidfodomrlemrALT  7233  exmidaclem  7238  exmidontriimlem3  7253  exmidontriimlem4  7254  exmidontriim  7255  pw1ne3  7260  sucpw1ne3  7262  sucpw1nel3  7263  onntri35  7267  elni2  7344  addnidpig  7366  elinp  7504  suplocexprlemdisj  7750  suplocexprlemub  7753  pitonn  7878  peano1nnnn  7882  peano2nnnn  7883  peano5nnnn  7922  sup3exmid  8945  peano5nni  8953  1nn  8961  peano2nn  8962  dfuzi  9394  uz11  9582  elfzonlteqm1  10242  frec2uzltd  10436  0tonninf  10472  1tonninf  10473  sumeq1  11398  prodeq1f  11595  ctiunct  12494  ssomct  12499  issubm  12939  isnsg  13158  releqgg  13176  eqgex  13177  resghm  13216  ghmeql  13223  issubrg  13585  lmodfopnelem2  13658  islssm  13690  islssmg  13691  lspsneq0  13759  istopg  13976  fiinbas  14026  topbas  14044  epttop  14067  restbasg  14145  icnpimaex  14188  lmcvg  14194  iscnp4  14195  cncnpi  14205  cnconst2  14210  cnptoprest  14216  cnptoprest2  14217  cnpdis  14219  lmss  14223  lmff  14226  txbas  14235  eltx  14236  txcnp  14248  txlm  14256  blssps  14404  blss  14405  blssexps  14406  blssex  14407  neibl  14468  metss  14471  metrest  14483  xmettx  14487  metcnp3  14488  tgioo  14523  tgqioo  14524  bdsep2  15116  bdzfauscl  15120  bj-indeq  15159  bj-nn0suc0  15180  bj-nnelirr  15183  bj-peano4  15185  bj-inf2vnlem2  15201  bj-nn0sucALT  15208  bj-findis  15209  strcollnft  15214  sscoll2  15218  nninfsellemdc  15238  nninfsellemqall  15243