Theorem eleq1 2301

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq1	|- ( A = B -> ( A e. C <-> B e. C ) )

Proof of Theorem eleq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2248	. . . 4 |- ( A = B -> ( x = A <-> x = B ) )
2	1	anbi1d 469	. . 3 |- ( A = B -> ( ( x = A /\ x e. C ) <-> ( x = B /\ x e. C ) ) )
3	2	exbidv 1878	. 2 |- ( A = B -> ( E. x ( x = A /\ x e. C ) <-> E. x ( x = B /\ x e. C ) ) )
4		df-clel 2234	. 2 |- ( A e. C <-> E. x ( x = A /\ x e. C ) )
5		df-clel 2234	. 2 |- ( B e. C <-> E. x ( x = B /\ x e. C ) )
6	3, 4, 5	3bitr4g 223	1 |- ( A = B -> ( A e. C <-> B e. C ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = 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  eleq1i  2304  eleq1d  2307  eleq1a  2310  cleqh  2338  nelneq  2339  clelsb1  2343  nfcjust  2380  cleqf  2417  nelne2  2511  neleq1  2519  rgen2a  2604  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  eqvisset  2832  ceqsralt  2849  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  rspce  2924  rspc2gv  2942  ceqsrexv  2956  ceqsrexbv  2957  clel2  2959  elabgt  2967  elabgf  2968  elrabi  2979  elrabf  2980  elrab3t  2981  ralab2  2990  rexab2  2992  mo2icl  3005  morex  3010  reu2  3014  reu6  3015  rmo4  3019  reu8  3022  reuind  3031  nelrdva  3033  ru  3050  dfsbcq  3053  dfsbcq2  3054  sbc8g  3059  sbcel1v  3114  rmob  3145  difjust  3221  unjust  3223  injust  3225  eldif  3229  dfssf  3238  dfss2f  3239  uniiunlem  3338  elun  3370  elin  3412  rabn0m  3549  disjne  3578  r19.3rm  3616  r19.9rmv  3619  raaanlem  3632  raaan  3633  elif  3652  ifmdc  3683  elpwg  3696  elpr2  3730  elsn2g  3741  rabsn  3775  tpid3g  3826  snssb  3846  snssgOLD  3849  difsn  3850  sssnm  3877  opeq1  3902  opeq2  3903  eluni  3936  elunii  3938  eluniab  3945  elint  3974  elintg  3976  elintab  3979  elintrabg  3981  intss1  3983  eliun  4014  eliin  4015  dfiunv2  4046  opabss  4193  cbvmpt  4224  trel  4234  trss  4236  ssex  4268  intnexr  4285  intexabim  4286  exmidel  4340  euabex  4363  elopab  4398  opelopab2a  4405  frirrg  4493  tz7.2  4497  ordelord  4524  onm  4544  ralxfr2d  4608  rexxfr2d  4609  rabxfrd  4613  reuhypd  4615  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  ontr2exmid  4670  onsucsssucexmid  4672  onsucelsucexmid  4675  ordsucunielexmid  4676  regexmidlem1  4678  elirr  4686  nordeq  4689  sucprcreg  4694  en2lp  4699  ordsoexmid  4707  ordsuc  4708  onsucuni2  4709  tfis  4728  peano2  4740  findes  4748  limom  4759  opelxp  4802  opeliunxp  4828  opbrop  4852  ssrel  4861  ssrel2  4863  ssrelrel  4873  relopabi  4903  eliunxp  4917  opeliunxp2  4918  ideqg  4929  reldmm  4998  dmmrnm  4999  dmxpm  5000  elreldm  5006  elrnmptg  5032  elres  5097  resiexg  5106  dfres2  5113  imai  5141  elimasng  5153  issref  5168  xpmlem  5206  xpm  5207  elxp4  5273  elxp5  5274  unielrel  5313  relcnvexb  5325  dmfex  5580  funfveu  5706  funimass4  5750  fvelimab  5756  ssimaex  5761  fvopab3g  5775  fvopab3ig  5776  fvmptssdm  5787  chfnrn  5814  fvelrn  5833  fmpt  5852  ffnfv  5860  fmptco  5868  elunirn  5965  f1elima  5972  cbvriota  6043  acexmidlemab  6072  acexmidlemcase  6073  cbvmpox  6159  eloprabga  6168  resoprab  6177  elrnmpo  6195  ov  6201  ovig  6203  ov6g  6220  ovg  6221  ovelrn  6231  caovimo  6276  abrexss  6351  fo1stresm  6388  fo2ndresm  6389  elxp6  6396  unielxp  6401  eqop2  6405  dfoprab4  6419  dfoprab4f  6420  fmpox  6429  1stconst  6450  2ndconst  6451  f1o2ndf1  6457  xporderlem  6460  f1od2  6464  disjxp1  6465  opeliunxp2f  6502  dftpos3  6526  dftpos4  6527  tpostpos  6528  smoel  6564  tfr1onlemaccex  6612  tfrcllemaccex  6625  tfrcl  6628  frecabcl  6663  frecsuc  6671  nntri3or  6759  nntri3  6763  nndcel  6766  riinerm  6875  th3qlem1  6904  mapsncnv  6970  elixpsn  7010  dom2lem  7051  fiprc  7097  xpsnen  7112  phplem3g  7150  phpelm  7161  ssfiexmid  7171  ssfiexmidt  7173  domfiexmid  7175  elssdc  7202  inffiexmid  7206  undifdcss  7223  opabfi  7240  snon0  7242  f1dmvrnfibi  7251  f1vrnfibi  7252  suppeqfsuppbi  7288  ordiso2  7368  ctssdclemn0  7443  ctssdc  7446  enumct  7448  nnnninf  7459  nnnninfeq  7461  nninfisollemne  7464  nninfisol  7466  finomni  7473  exmidlpo  7476  pr2cv1  7534  acneq  7551  finacn  7553  acfun  7556  exmidontriimlem3  7572  exmidontriimlem4  7573  pw1ne1  7581  onntri35  7589  exmidapne  7619  ccfunen  7623  cc2lem  7625  elni2  7674  recexnq  7750  recmulnqg  7751  enq0enq  7791  enq0sym  7792  enq0ref  7793  enq0tr  7794  enq0breq  7796  nqnq0pi  7798  nqnq0  7801  prop  7835  prcdnql  7844  prcunqu  7845  prubl  7846  prltlu  7847  prnmaxl  7848  prnminu  7849  prdisj  7852  prarloc  7863  genipv  7869  genpelvl  7872  genpelvu  7873  genprndl  7881  genprndu  7882  distrlem5prl  7946  distrlem5pru  7947  ltexprlemm  7960  ltexprlemdisj  7966  ltexprlemloc  7967  ltexprlemrl  7970  ltexprlemru  7972  aptiprleml  7999  aptiprlemu  8000  archpr  8003  cauappcvgprlemm  8005  cauappcvgprlemladdfu  8014  cauappcvgprlemladdfl  8015  caucvgprlemm  8028  caucvgprlemladdfu  8037  caucvgprprlemmu  8055  elreal2  8190  ltresr  8199  axcnre  8241  axpre-suploclemres  8261  0re  8319  renepnf  8366  renemnf  8367  ltxrlt  8384  eqlei2  8413  0cnALT  8509  sup3exmid  9280  nn1suc  9305  nnne0  9314  xnn0xr  9617  nn0nepnf  9620  elz  9628  elnn0z  9639  elz2  9698  uzind4s  9972  elnn1uz2  9989  qre  10007  elpqb  10032  xnn0lenn0nn0  10249  xsubge0  10265  xposdif  10266  xleaddadd  10271  fzsn  10453  fz1sbc  10484  elfzp12  10487  fzm1  10488  fz01or  10499  fvinim0ffz  10641  suprzubdc  10652  zsupssdc  10654  xqltnle  10683  flqidz  10702  ceilqidz  10734  modqmuladdnn0  10786  frec2uzrand  10823  frecuzrdgtcl  10830  fzfig  10848  seq3fveq2  10893  seqfveq2g  10895  seq3shft2  10899  seqshft2g  10900  monoord  10903  seq3split  10906  seqsplitg  10907  iseqf1olemqval  10918  seq3id2  10944  seqhomog  10948  1exp  10986  bcval  11168  hashennn  11200  hashfibc  11264  zfz1isolem1  11273  zfz1iso  11274  seq3coll  11275  iswrdiz  11292  0wrd0  11311  lswlgt0cl  11338  ccatval1  11346  ccatval2  11347  ccatalpha  11362  ccatrcl1  11363  wrdl1s1  11379  ccats1val2  11389  wrd2ind  11476  pfxccatin12lem3  11485  pfxccatid  11494  reuccatpfxs1lem  11499  shftlem  11562  shftfibg  11566  shftfib  11569  shftfn  11570  2shfti  11577  rexuz3  11737  sqrt0rlem  11750  cau3  11862  negfi  11975  sumdc  12105  sumrbdclem  12125  summodclem2a  12129  fisumss  12140  prodrbdclem  12319  prodmodclem2a  12324  fprodssdc  12338  fprodsplit1f  12382  ef0lem  12408  odd2np1  12621  even2n  12622  oddnn02np1  12628  oddge22np1  12629  evennn02n  12630  evennn2n  12631  nn0enne  12650  divalgmod  12675  uzwodc  12795  lcmgcdlem  12836  cncongr1  12862  1nprm  12873  isprm2  12876  dvdsnprmd  12884  prmdc  12889  exprmfct  12897  nprmdvds1  12899  coprm  12903  prmdiveq  12995  prm23lt5  13023  pcpre1  13052  pc2dvds  13090  pcz  13092  pcmpt  13103  qexpz  13112  4sqlem2  13149  4sqlem19  13169  ballotfilem2  13209  ballotfilemfc0  13213  ballotfilemfcc  13214  ennnfonelemhom  13287  ctiunctlemudc  13309  ssnnctlemct  13318  nninfdclemcl  13320  imasaddfnlemg  13615  ismgmid  13677  isgrpid2  13825  mhmlem  13897  eqgval  14006  dvdsrcl2  14382  nzrunit  14471  lringuplu  14479  dvdsrzring  14913  znrrg  14970  mplsubgfilemm  15015  fiinopn  15031  istopon  15040  basis2  15075  eltg3  15084  tg2  15087  tgidm  15101  bastop  15102  bastop2  15111  topnex  15113  isopn3  15152  tgrest  15196  cnpval  15225  lmbr  15240  cnconst  15261  txbas  15285  uptx  15301  txdis1cn  15305  cnmpt12  15314  cnmpt22  15321  hmeocnvb  15345  xblm  15444  isxms2  15479  mopni  15509  blssioo  15580  dedekindeulemuub  15644  dedekindeulemeu  15649  dedekindicclemuub  15653  dedekindicclemeu  15658  ivthinclemlm  15661  ivthinclemum  15662  ivthreinc  15672  pellexlem3  16010  lgsfvalg  16041  lgsval2lem  16046  lgsdir2lem2  16065  gausslemma2dlem1a  16094  gausslemma2dlem4  16100  gausslemma2dlem6  16103  2lgslem1b  16125  2lgs  16140  2lgsoddprmlem2  16142  2lgsoddprmlem3  16147  2sqlem2  16151  2sqlem6  16156  2sqlem7  16157  2sqlem10  16161  vtxvalg  16174  iedgvalg  16175  umgredg  16303  upgrpredgv  16304  usgredg2vlem2  16381  ushgredgedg  16384  ushgredgedgloop  16386  griedg0ssusgr  16409  uhgrspansubgrlem  16434  vtxdgfifival  16449  iswlk  16481  upgrwlkvtxedg  16522  isclwwlknx  16574  clwwlkn1loopb  16578  clwwlknonex2lem1  16595  elabgf0  16722  bj-rspgt  16731  cbvrald  16733  decidi  16740  sumdc2  16744  bdssex  16845  bj-inex  16850  bj-intnexr  16852  bj-unexg  16864  bj-d0clsepcl  16868  bj-nnelirr  16896  bj-nn0suc  16907  bj-inf2vnlem1  16913  bj-inf2vnlem2  16914  bj-inf2vnlem3  16915  bj-inf2vnlem4  16916  bj-nn0sucALT  16921  bj-findis  16922  3dom  16935  trilpolemcl  16994