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  2669  rexeqf  2670  reueq1f  2671  rmoeq1f  2672  rabeqf  2728  clel3g  2872  clel4  2874  sbcbi2  3014  sbcel2gv  3027  csbeq2  3082  sbnfc2  3118  difeq2  3248  uneq1  3283  ineq1  3330  nel02  3428  n0i  3429  disjel  3478  exsnrex  3635  sneqr  3761  preqr1g  3767  preqr1  3769  preq12b  3771  prel12  3772  elunii  3815  eluniab  3822  ssuni  3832  elinti  3854  elintab  3856  intss1  3860  intmin  3865  intab  3874  iineq2  3904  dfiin2g  3920  breq  4006  axsep2  4123  zfauscl  4124  inuni  4156  exmidexmid  4197  ss1o0el1  4198  exmid01  4199  exmidundif  4207  exmidundifim  4208  rext  4216  intid  4225  mss  4227  opth1  4237  opeqex  4250  frforeq3  4348  frirrg  4351  limeq  4378  nsuceq0g  4419  suctr  4422  snnex  4449  uniuni  4452  iunpw  4481  ordtriexmidlem  4519  ordtriexmidlem2  4520  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  ontr2exmid  4525  ordtri2or2exmidlem  4526  onsucelsucexmidlem  4529  onsucelsucexmid  4530  ordsucunielexmid  4531  regexmidlem1  4533  reg2exmidlema  4534  regexmid  4535  reg2exmid  4536  elirr  4541  en2lp  4554  suc11g  4557  dtruex  4559  ordsoexmid  4562  nlimsucg  4566  onintexmid  4573  reg3exmidlemwe  4579  reg3exmid  4580  peano5  4598  limom  4614  0elnn  4619  nn0eln0  4620  nnregexmid  4621  xpeq1  4641  xpeq2  4642  opthprc  4678  xp11m  5068  funopg  5251  dffo4  5665  elunirn  5767  f1oiso  5827  canth  5829  eusvobj2  5861  acexmidlema  5866  acexmidlemb  5867  acexmidlemab  5869  acexmidlem2  5872  mpoeq123  5934  oprssdmm  6172  unielxp  6175  cnvf1o  6226  smoel  6301  tfr0dm  6323  frecabcl  6400  nnsucelsuc  6492  nntri3or  6494  nntri2  6495  nntri3  6498  nndceq  6500  nnmordi  6517  nnaordex  6529  elqsn0m  6603  qsel  6612  mapsn  6690  findcard2s  6890  undifdcss  6922  ctssdclemr  7111  nnnninf2  7125  exmidonfinlem  7192  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  exmidontriimlem3  7222  exmidontriimlem4  7223  exmidontriim  7224  pw1ne3  7229  sucpw1ne3  7231  sucpw1nel3  7232  onntri35  7236  elni2  7313  addnidpig  7335  elinp  7473  suplocexprlemdisj  7719  suplocexprlemub  7722  pitonn  7847  peano1nnnn  7851  peano2nnnn  7852  peano5nnnn  7891  sup3exmid  8914  peano5nni  8922  1nn  8930  peano2nn  8931  dfuzi  9363  uz11  9550  elfzonlteqm1  10210  frec2uzltd  10403  0tonninf  10439  1tonninf  10440  sumeq1  11363  prodeq1f  11560  ctiunct  12441  ssomct  12446  issubm  12863  isnsg  13062  releqgg  13080  issubrg  13342  lmodfopnelem2  13415  istopg  13502  fiinbas  13552  topbas  13570  epttop  13593  restbasg  13671  icnpimaex  13714  lmcvg  13720  iscnp4  13721  cncnpi  13731  cnconst2  13736  cnptoprest  13742  cnptoprest2  13743  cnpdis  13745  lmss  13749  lmff  13752  txbas  13761  eltx  13762  txcnp  13774  txlm  13782  blssps  13930  blss  13931  blssexps  13932  blssex  13933  neibl  13994  metss  13997  metrest  14009  xmettx  14013  metcnp3  14014  tgioo  14049  tgqioo  14050  bdsep2  14641  bdzfauscl  14645  bj-indeq  14684  bj-nn0suc0  14705  bj-nnelirr  14708  bj-peano4  14710  bj-inf2vnlem2  14726  bj-nn0sucALT  14733  bj-findis  14734  strcollnft  14739  sscoll2  14743  nninfsellemdc  14762  nninfsellemqall  14767