Theorem eleq1 2259

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

Assertion

Ref	Expression
eleq1	⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2206	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 465	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1839	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2192	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2192	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364  ∃wex 1506   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12  2261  eleq1i  2262  eleq1d  2265  eleq1a  2268  cleqh  2296  nelneq  2297  clelsb1  2301  nfcjust  2327  cleqf  2364  nelne2  2458  neleq1  2466  rgen2a  2551  cbvralf  2721  cbvrexf  2722  cbvreu  2727  cbvrab  2761  eqvisset  2773  ceqsralt  2790  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  rspce  2863  rspc2gv  2880  ceqsrexv  2894  ceqsrexbv  2895  clel2  2897  elabgt  2905  elabgf  2906  elrabi  2917  elrabf  2918  elrab3t  2919  ralab2  2928  rexab2  2930  mo2icl  2943  morex  2948  reu2  2952  reu6  2953  rmo4  2957  reu8  2960  reuind  2969  nelrdva  2971  ru  2988  dfsbcq  2991  dfsbcq2  2992  sbc8g  2997  sbcel1v  3052  rmob  3082  difjust  3158  unjust  3160  injust  3162  eldif  3166  dfss2f  3175  uniiunlem  3273  elun  3305  elin  3347  rabn0m  3479  disjne  3505  r19.3rm  3540  r19.9rmv  3543  raaanlem  3556  raaan  3557  ifmdc  3602  elpwg  3614  elpr2  3645  elsn2g  3656  rabsn  3690  tpid3g  3738  snssb  3756  snssgOLD  3759  difsn  3760  sssnm  3785  opeq1  3809  opeq2  3810  eluni  3843  elunii  3845  eluniab  3852  elint  3881  elintg  3883  elintab  3886  elintrabg  3888  intss1  3890  eliun  3921  eliin  3922  dfiunv2  3953  opabss  4098  cbvmpt  4129  trel  4139  trss  4141  ssex  4171  intnexr  4185  intexabim  4186  exmidel  4239  euabex  4259  elopab  4293  opelopab2a  4300  frirrg  4386  tz7.2  4390  ordelord  4417  onm  4437  ralxfr2d  4500  rexxfr2d  4501  rabxfrd  4505  reuhypd  4507  ordtriexmid  4558  ontriexmidim  4559  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  onsucelsucexmid  4567  ordsucunielexmid  4568  regexmidlem1  4570  elirr  4578  nordeq  4581  sucprcreg  4586  en2lp  4591  ordsoexmid  4599  ordsuc  4600  onsucuni2  4601  tfis  4620  peano2  4632  findes  4640  limom  4651  opelxp  4694  opeliunxp  4719  opbrop  4743  ssrel  4752  ssrel2  4754  ssrelrel  4764  relopabi  4792  eliunxp  4806  opeliunxp2  4807  ideqg  4818  dmmrnm  4886  dmxpm  4887  elreldm  4893  elrnmptg  4919  elres  4983  resiexg  4992  dfres2  4999  imai  5026  elimasng  5038  issref  5053  xpmlem  5091  xpm  5092  elxp4  5158  elxp5  5159  unielrel  5198  relcnvexb  5210  dmfex  5450  funfveu  5574  funimass4  5614  fvelimab  5620  ssimaex  5625  fvopab3g  5637  fvopab3ig  5638  fvmptssdm  5649  chfnrn  5676  fvelrn  5696  fmpt  5715  ffnfv  5723  fmptco  5731  elunirn  5816  f1elima  5823  cbvriota  5891  acexmidlemab  5919  acexmidlemcase  5920  cbvmpox  6004  eloprabga  6013  resoprab  6022  elrnmpo  6040  ov  6046  ovig  6048  ov6g  6065  ovg  6066  ovelrn  6076  caovimo  6121  fo1stresm  6228  fo2ndresm  6229  elxp6  6236  unielxp  6241  eqop2  6245  dfoprab4  6259  dfoprab4f  6260  fmpox  6267  1stconst  6288  2ndconst  6289  f1o2ndf1  6295  xporderlem  6298  f1od2  6302  disjxp1  6303  opeliunxp2f  6305  dftpos3  6329  dftpos4  6330  tpostpos  6331  smoel  6367  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfrcl  6431  frecabcl  6466  frecsuc  6474  nntri3or  6560  nntri3  6564  nndcel  6567  riinerm  6676  th3qlem1  6705  mapsncnv  6763  elixpsn  6803  dom2lem  6840  fiprc  6883  xpsnen  6889  phplem3g  6926  phpelm  6936  ssfiexmid  6946  domfiexmid  6948  inffiexmid  6976  undifdcss  6993  opabfi  7008  snon0  7010  f1dmvrnfibi  7019  f1vrnfibi  7020  ordiso2  7110  ctssdclemn0  7185  ctssdc  7188  enumct  7190  nnnninf  7201  nnnninfeq  7203  nninfisollemne  7206  nninfisol  7208  finomni  7215  exmidlpo  7218  acneq  7287  finacn  7289  acfun  7292  exmidontriimlem3  7308  exmidontriimlem4  7309  pw1ne1  7314  onntri35  7322  exmidapne  7345  ccfunen  7349  cc2lem  7351  elni2  7400  recexnq  7476  recmulnqg  7477  enq0enq  7517  enq0sym  7518  enq0ref  7519  enq0tr  7520  enq0breq  7522  nqnq0pi  7524  nqnq0  7527  prop  7561  prcdnql  7570  prcunqu  7571  prubl  7572  prltlu  7573  prnmaxl  7574  prnminu  7575  prdisj  7578  prarloc  7589  genipv  7595  genpelvl  7598  genpelvu  7599  genprndl  7607  genprndu  7608  distrlem5prl  7672  distrlem5pru  7673  ltexprlemm  7686  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemrl  7696  ltexprlemru  7698  aptiprleml  7725  aptiprlemu  7726  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemm  7754  caucvgprlemladdfu  7763  caucvgprprlemmu  7781  elreal2  7916  ltresr  7925  axcnre  7967  axpre-suploclemres  7987  0re  8045  renepnf  8093  renemnf  8094  ltxrlt  8111  eqlei2  8140  0cnALT  8235  sup3exmid  9003  nn1suc  9028  nnne0  9037  xnn0xr  9336  nn0nepnf  9339  elz  9347  elnn0z  9358  elz2  9416  uzind4s  9683  elnn1uz2  9700  qre  9718  elpqb  9743  xnn0lenn0nn0  9959  xsubge0  9975  xposdif  9976  xleaddadd  9981  fzsn  10160  fz1sbc  10190  elfzp12  10193  fzm1  10194  fz01or  10205  fvinim0ffz  10336  suprzubdc  10345  zsupssdc  10347  xqltnle  10376  flqidz  10395  ceilqidz  10427  modqmuladdnn0  10479  frec2uzrand  10516  frecuzrdgtcl  10523  fzfig  10541  seq3fveq2  10586  seqfveq2g  10588  seq3shft2  10592  seqshft2g  10593  monoord  10596  seq3split  10599  seqsplitg  10600  iseqf1olemqval  10611  seq3id2  10637  seqhomog  10641  1exp  10679  bcval  10860  hashennn  10891  zfz1isolem1  10951  zfz1iso  10952  seq3coll  10953  iswrdiz  10961  0wrd0  10980  shftlem  11000  shftfibg  11004  shftfib  11007  shftfn  11008  2shfti  11015  rexuz3  11174  sqrt0rlem  11187  cau3  11299  negfi  11412  sumdc  11542  sumrbdclem  11561  summodclem2a  11565  fisumss  11576  prodrbdclem  11755  prodmodclem2a  11760  fprodssdc  11774  fprodsplit1f  11818  ef0lem  11844  odd2np1  12057  even2n  12058  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  nn0enne  12086  divalgmod  12111  uzwodc  12231  lcmgcdlem  12272  cncongr1  12298  1nprm  12309  isprm2  12312  dvdsnprmd  12320  prmdc  12325  exprmfct  12333  nprmdvds1  12335  coprm  12339  prmdiveq  12431  prm23lt5  12459  pcpre1  12488  pc2dvds  12526  pcz  12528  pcmpt  12539  qexpz  12548  4sqlem2  12585  4sqlem19  12605  ennnfonelemhom  12659  ctiunctlemudc  12681  ssnnctlemct  12690  nninfdclemcl  12692  imasaddfnlemg  13018  ismgmid  13081  isgrpid2  13244  mhmlem  13322  eqgval  13431  dvdsrcl2  13733  nzrunit  13822  lringuplu  13830  dvdsrzring  14237  znrrg  14294  mplsubgfilemm  14332  fiinopn  14348  istopon  14357  basis2  14392  eltg3  14401  tg2  14404  tgidm  14418  bastop  14419  bastop2  14428  topnex  14430  isopn3  14469  tgrest  14513  cnpval  14542  lmbr  14557  cnconst  14578  txbas  14602  uptx  14618  txdis1cn  14622  cnmpt12  14631  cnmpt22  14638  hmeocnvb  14662  xblm  14761  isxms2  14796  mopni  14826  blssioo  14897  dedekindeulemuub  14961  dedekindeulemeu  14966  dedekindicclemuub  14970  dedekindicclemeu  14975  ivthinclemlm  14978  ivthinclemum  14979  ivthreinc  14989  lgsfvalg  15354  lgsval2lem  15359  lgsdir2lem2  15378  gausslemma2dlem1a  15407  gausslemma2dlem4  15413  gausslemma2dlem6  15416  2lgslem1b  15438  2lgs  15453  2lgsoddprmlem2  15455  2lgsoddprmlem3  15460  2sqlem2  15464  2sqlem6  15469  2sqlem7  15470  2sqlem10  15474  elabgf0  15531  bj-rspgt  15540  cbvrald  15542  decidi  15549  sumdc2  15553  bdssex  15656  bj-inex  15661  bj-intnexr  15663  bj-unexg  15675  bj-d0clsepcl  15679  bj-nnelirr  15707  bj-nn0suc  15718  bj-inf2vnlem1  15724  bj-inf2vnlem2  15725  bj-inf2vnlem3  15726  bj-inf2vnlem4  15727  bj-nn0sucALT  15732  bj-findis  15733  trilpolemcl  15794