Theorem eleq2 2302

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 2232	. . . . . 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 1611	. . . 4 |- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi2d 468	. . 3 |- ( A = B -> ( ( x = C /\ x e. A ) <-> ( x = C /\ x e. B ) ) )
5	4	exbidv 1878	. 2 |- ( A = B -> ( E. x ( x = C /\ x e. A ) <-> E. x ( x = C /\ x e. B ) ) )
6		df-clel 2234	. 2 |- ( C e. A <-> E. x ( x = C /\ x e. A ) )
7		df-clel 2234	. 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 1400   = wceq 1402   E.wex 1545   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is referenced by:  eleq12  2303  eleq2i  2305  eleq2d  2308  nelneq2  2340  clelsb2  2344  dvelimdc  2413  nelne1  2510  neleq2  2520  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2811  clel3g  2960  clel4  2962  sbcbi2  3102  sbcel2gv  3115  csbeq2  3171  sbnfc2  3208  difeq2  3341  uneq1  3376  ineq1  3425  nel02  3526  n0i  3527  disjel  3579  exsnrex  3750  sneqr  3883  preqr1g  3889  preqr1  3891  preq12b  3893  prel12  3894  elunii  3938  eluniab  3945  ssuni  3955  elinti  3977  elintab  3979  intss1  3983  intmin  3988  intab  3997  iineq2  4027  dfiin2g  4043  breq  4130  axsepg  4248  sepg  4249  zfausclOLD  4251  inuni  4289  exmidexmid  4331  ss1o0el1  4332  exmid01  4333  exmidundif  4341  exmidundifim  4342  rext  4353  intid  4362  mss  4364  opth1  4374  opeqex  4388  frforeq3  4490  frirrg  4493  limeq  4520  nsuceq0g  4561  suctr  4564  snnex  4592  uniuni  4595  iunpw  4624  ordtriexmidlem  4664  ordtriexmidlem2  4665  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  ontr2exmid  4670  ordtri2or2exmidlem  4671  onsucelsucexmidlem  4674  onsucelsucexmid  4675  ordsucunielexmid  4676  regexmidlem1  4678  reg2exmidlema  4679  regexmid  4680  reg2exmid  4681  elirr  4686  en2lp  4699  suc11g  4702  dtruex  4704  ordsoexmid  4707  nlimsucg  4711  onintexmid  4718  reg3exmidlemwe  4724  reg3exmid  4725  peano5  4743  limom  4759  0elnn  4764  nn0eln0  4765  nnregexmid  4766  xpeq1  4786  xpeq2  4787  opthprc  4824  xp11m  5224  funopg  5409  dffo4  5850  funopdmsn  5889  elunirn  5965  f1oiso  6025  canth  6029  eusvobj2  6064  acexmidlema  6069  acexmidlemb  6070  acexmidlemab  6072  acexmidlem2  6075  mpoeq123  6140  oprssdmm  6398  unielxp  6401  cnvf1o  6454  smoel  6564  tfr0dm  6586  frecabcl  6663  nnsucelsuc  6757  nntri3or  6759  nntri2  6760  nntri3  6763  nndceq  6765  nnmordi  6782  nnaordex  6794  elqsn0m  6870  qsel  6879  mapsnd  6963  mapsn  6965  en2m  7106  pw2f1odclem  7127  findcard2s  7187  elssdc  7202  eqsndc  7203  undifdcss  7223  fissfi  7256  2omap  7311  ctssdclemr  7445  nnnninf2  7460  exmidonfinlem  7538  exmidfodomrlemr  7547  exmidfodomrlemrALT  7548  finacn  7553  exmidaclem  7557  exmidontriimlem3  7572  exmidontriimlem4  7573  exmidontriim  7574  iftrueb01  7575  pw1ne3  7582  sucpw1ne3  7584  sucpw1nel3  7585  onntri35  7589  acnccim  7631  elni2  7674  addnidpig  7696  elinp  7834  suplocexprlemdisj  8080  suplocexprlemub  8083  pitonn  8208  peano1nnnn  8212  peano2nnnn  8213  peano5nnnn  8252  sup3exmid  9280  peano5nni  9289  1nn  9297  peano2nn  9298  dfuzi  9738  uz11  9927  elfzonlteqm1  10609  frec2uzltd  10821  0tonninf  10858  1tonninf  10859  hashfibclem  11263  hashf1lem2  11267  wrdsymb0  11318  lsw0  11333  swrdwrdsymbg  11417  sumeq1  12102  prodeq1f  12300  nninfctlemfo  12798  ballotfilemcdc  13204  ballotfilem7  13260  ctiunct  13312  ssomct  13317  issubm  13759  isnsg  13985  releqgg  14003  eqgex  14004  resghm  14043  ghmeql  14050  issubrg  14505  lmodfopnelem2  14637  islssm  14669  islssmg  14670  lspsneq0  14738  istopg  15026  fiinbas  15076  topbas  15094  epttop  15117  restbasg  15195  icnpimaex  15238  lmcvg  15244  iscnp4  15245  cncnpi  15255  cnconst2  15260  cnptoprest  15266  cnptoprest2  15267  cnpdis  15269  lmss  15273  lmff  15276  txbas  15285  eltx  15286  txcnp  15298  txlm  15306  blssps  15454  blss  15455  blssexps  15456  blssex  15457  neibl  15518  metss  15521  metrest  15533  xmettx  15537  metcnp3  15538  tgioo  15581  tgqioo  15582  uhgrm  16236  lpvtx  16237  incistruhgr  16248  umgrnloopv  16272  uhgredgm  16294  uhgrvtxedgiedgb  16301  upgredg2vtx  16306  uhgr2edg  16364  umgrvad2edg  16369  usgredg4  16373  uspgredg2vlem  16378  ushgredgedg  16384  subgruhgredgdm  16428  vtxd0nedgbfi  16457  1loopgrvd2fi  16463  wlk1walkdom  16517  bdsep2  16829  bdsepg  16833  bj-indeq  16872  bj-nn0suc0  16893  bj-nnelirr  16896  bj-peano4  16898  bj-inf2vnlem2  16914  bj-nn0sucALT  16921  bj-findis  16922  strcollnft  16927  sscoll2  16931  nninfsellemdc  16961  nninfsellemqall  16966  nnnninfex  16973