Theorem eleq2 2269

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 2199	. . . . . 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 1581	. . . 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 1848	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2201	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2201	. 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 1371   = wceq 1373   E.wex 1515   e. wcel 2176

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  eleq12  2270  eleq2i  2272  eleq2d  2275  nelneq2  2307  clelsb2  2311  dvelimdc  2369  nelne1  2466  neleq2  2476  raleqf  2698  rexeqf  2699  reueq1f  2700  rmoeq1f  2701  rabeqf  2762  clel3g  2907  clel4  2909  sbcbi2  3049  sbcel2gv  3062  csbeq2  3117  sbnfc2  3154  difeq2  3285  uneq1  3320  ineq1  3367  nel02  3465  n0i  3466  disjel  3515  exsnrex  3675  sneqr  3801  preqr1g  3807  preqr1  3809  preq12b  3811  prel12  3812  elunii  3855  eluniab  3862  ssuni  3872  elinti  3894  elintab  3896  intss1  3900  intmin  3905  intab  3914  iineq2  3944  dfiin2g  3960  breq  4046  axsep2  4163  zfauscl  4164  inuni  4199  exmidexmid  4240  ss1o0el1  4241  exmid01  4242  exmidundif  4250  exmidundifim  4251  rext  4259  intid  4268  mss  4270  opth1  4280  opeqex  4294  frforeq3  4394  frirrg  4397  limeq  4424  nsuceq0g  4465  suctr  4468  snnex  4495  uniuni  4498  iunpw  4527  ordtriexmidlem  4567  ordtriexmidlem2  4568  ordtriexmid  4569  ontriexmidim  4570  ordtri2orexmid  4571  ontr2exmid  4573  ordtri2or2exmidlem  4574  onsucelsucexmidlem  4577  onsucelsucexmid  4578  ordsucunielexmid  4579  regexmidlem1  4581  reg2exmidlema  4582  regexmid  4583  reg2exmid  4584  elirr  4589  en2lp  4602  suc11g  4605  dtruex  4607  ordsoexmid  4610  nlimsucg  4614  onintexmid  4621  reg3exmidlemwe  4627  reg3exmid  4628  peano5  4646  limom  4662  0elnn  4667  nn0eln0  4668  nnregexmid  4669  xpeq1  4689  xpeq2  4690  opthprc  4726  xp11m  5121  funopg  5305  dffo4  5728  funopdmsn  5764  elunirn  5835  f1oiso  5895  canth  5897  eusvobj2  5930  acexmidlema  5935  acexmidlemb  5936  acexmidlemab  5938  acexmidlem2  5941  mpoeq123  6004  oprssdmm  6257  unielxp  6260  cnvf1o  6311  smoel  6386  tfr0dm  6408  frecabcl  6485  nnsucelsuc  6577  nntri3or  6579  nntri2  6580  nntri3  6583  nndceq  6585  nnmordi  6602  nnaordex  6614  elqsn0m  6690  qsel  6699  mapsn  6777  pw2f1odclem  6931  findcard2s  6987  undifdcss  7020  ctssdclemr  7214  nnnninf2  7229  exmidonfinlem  7301  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  finacn  7316  exmidaclem  7320  exmidontriimlem3  7335  exmidontriimlem4  7336  exmidontriim  7337  pw1ne3  7342  sucpw1ne3  7344  sucpw1nel3  7345  onntri35  7349  acnccim  7384  elni2  7427  addnidpig  7449  elinp  7587  suplocexprlemdisj  7833  suplocexprlemub  7836  pitonn  7961  peano1nnnn  7965  peano2nnnn  7966  peano5nnnn  8005  sup3exmid  9030  peano5nni  9039  1nn  9047  peano2nn  9048  dfuzi  9483  uz11  9671  elfzonlteqm1  10339  frec2uzltd  10548  0tonninf  10585  1tonninf  10586  wrdsymb0  11026  lsw0  11041  swrdwrdsymbg  11117  sumeq1  11666  prodeq1f  11863  nninfctlemfo  12361  ctiunct  12811  ssomct  12816  issubm  13304  isnsg  13538  releqgg  13556  eqgex  13557  resghm  13596  ghmeql  13603  issubrg  13983  lmodfopnelem2  14087  islssm  14119  islssmg  14120  lspsneq0  14188  istopg  14471  fiinbas  14521  topbas  14539  epttop  14562  restbasg  14640  icnpimaex  14683  lmcvg  14689  iscnp4  14690  cncnpi  14700  cnconst2  14705  cnptoprest  14711  cnptoprest2  14712  cnpdis  14714  lmss  14718  lmff  14721  txbas  14730  eltx  14731  txcnp  14743  txlm  14751  blssps  14899  blss  14900  blssexps  14901  blssex  14902  neibl  14963  metss  14966  metrest  14978  xmettx  14982  metcnp3  14983  tgioo  15026  tgqioo  15027  bdsep2  15826  bdzfauscl  15830  bj-indeq  15869  bj-nn0suc0  15890  bj-nnelirr  15893  bj-peano4  15895  bj-inf2vnlem2  15911  bj-nn0sucALT  15918  bj-findis  15919  strcollnft  15924  sscoll2  15928  2omap  15936  nninfsellemdc  15951  nninfsellemqall  15956  nnnninfex  15963