Theorem eleq1 2294

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 2241	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 465	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1873	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2227	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2227	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397  ∃wex 1540   ∈ wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  eleq12  2296  eleq1i  2297  eleq1d  2300  eleq1a  2303  cleqh  2331  nelneq  2332  clelsb1  2336  nfcjust  2362  cleqf  2399  nelne2  2493  neleq1  2501  rgen2a  2586  cbvralf  2758  cbvrexf  2759  cbvreu  2765  cbvrab  2800  eqvisset  2813  ceqsralt  2830  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  rspce  2905  rspc2gv  2922  ceqsrexv  2936  ceqsrexbv  2937  clel2  2939  elabgt  2947  elabgf  2948  elrabi  2959  elrabf  2960  elrab3t  2961  ralab2  2970  rexab2  2972  mo2icl  2985  morex  2990  reu2  2994  reu6  2995  rmo4  2999  reu8  3002  reuind  3011  nelrdva  3013  ru  3030  dfsbcq  3033  dfsbcq2  3034  sbc8g  3039  sbcel1v  3094  rmob  3125  difjust  3201  unjust  3203  injust  3205  eldif  3209  dfss2f  3218  uniiunlem  3316  elun  3348  elin  3390  rabn0m  3522  disjne  3548  r19.3rm  3583  r19.9rmv  3586  raaanlem  3599  raaan  3600  elif  3617  ifmdc  3648  elpwg  3660  elpr2  3691  elsn2g  3702  rabsn  3736  tpid3g  3787  snssb  3806  snssgOLD  3809  difsn  3810  sssnm  3837  opeq1  3862  opeq2  3863  eluni  3896  elunii  3898  eluniab  3905  elint  3934  elintg  3936  elintab  3939  elintrabg  3941  intss1  3943  eliun  3974  eliin  3975  dfiunv2  4006  opabss  4153  cbvmpt  4184  trel  4194  trss  4196  ssex  4226  intnexr  4241  intexabim  4242  exmidel  4295  euabex  4317  elopab  4352  opelopab2a  4359  frirrg  4447  tz7.2  4451  ordelord  4478  onm  4498  ralxfr2d  4561  rexxfr2d  4562  rabxfrd  4566  reuhypd  4568  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  onsucelsucexmid  4628  ordsucunielexmid  4629  regexmidlem1  4631  elirr  4639  nordeq  4642  sucprcreg  4647  en2lp  4652  ordsoexmid  4660  ordsuc  4661  onsucuni2  4662  tfis  4681  peano2  4693  findes  4701  limom  4712  opelxp  4755  opeliunxp  4781  opbrop  4805  ssrel  4814  ssrel2  4816  ssrelrel  4826  relopabi  4855  eliunxp  4869  opeliunxp2  4870  ideqg  4881  reldmm  4950  dmmrnm  4951  dmxpm  4952  elreldm  4958  elrnmptg  4984  elres  5049  resiexg  5058  dfres2  5065  imai  5092  elimasng  5104  issref  5119  xpmlem  5157  xpm  5158  elxp4  5224  elxp5  5225  unielrel  5264  relcnvexb  5276  dmfex  5526  funfveu  5652  funimass4  5696  fvelimab  5702  ssimaex  5707  fvopab3g  5719  fvopab3ig  5720  fvmptssdm  5731  chfnrn  5758  fvelrn  5778  fmpt  5797  ffnfv  5805  fmptco  5813  elunirn  5906  f1elima  5913  cbvriota  5982  acexmidlemab  6011  acexmidlemcase  6012  cbvmpox  6098  eloprabga  6107  resoprab  6116  elrnmpo  6134  ov  6140  ovig  6142  ov6g  6159  ovg  6160  ovelrn  6170  caovimo  6215  fo1stresm  6323  fo2ndresm  6324  elxp6  6331  unielxp  6336  eqop2  6340  dfoprab4  6354  dfoprab4f  6355  fmpox  6364  1stconst  6385  2ndconst  6386  f1o2ndf1  6392  xporderlem  6395  f1od2  6399  disjxp1  6400  opeliunxp2f  6403  dftpos3  6427  dftpos4  6428  tpostpos  6429  smoel  6465  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfrcl  6529  frecabcl  6564  frecsuc  6572  nntri3or  6660  nntri3  6664  nndcel  6667  riinerm  6776  th3qlem1  6805  mapsncnv  6863  elixpsn  6903  dom2lem  6944  fiprc  6989  xpsnen  7004  phplem3g  7041  phpelm  7052  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  elssdc  7093  inffiexmid  7097  undifdcss  7114  opabfi  7131  snon0  7133  f1dmvrnfibi  7142  f1vrnfibi  7143  ordiso2  7233  ctssdclemn0  7308  ctssdc  7311  enumct  7313  nnnninf  7324  nnnninfeq  7326  nninfisollemne  7329  nninfisol  7331  finomni  7338  exmidlpo  7341  pr2cv1  7399  acneq  7416  finacn  7418  acfun  7421  exmidontriimlem3  7437  exmidontriimlem4  7438  pw1ne1  7446  onntri35  7454  exmidapne  7478  ccfunen  7482  cc2lem  7484  elni2  7533  recexnq  7609  recmulnqg  7610  enq0enq  7650  enq0sym  7651  enq0ref  7652  enq0tr  7653  enq0breq  7655  nqnq0pi  7657  nqnq0  7660  prop  7694  prcdnql  7703  prcunqu  7704  prubl  7705  prltlu  7706  prnmaxl  7707  prnminu  7708  prdisj  7711  prarloc  7722  genipv  7728  genpelvl  7731  genpelvu  7732  genprndl  7740  genprndu  7741  distrlem5prl  7805  distrlem5pru  7806  ltexprlemm  7819  ltexprlemdisj  7825  ltexprlemloc  7826  ltexprlemrl  7829  ltexprlemru  7831  aptiprleml  7858  aptiprlemu  7859  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  caucvgprlemm  7887  caucvgprlemladdfu  7896  caucvgprprlemmu  7914  elreal2  8049  ltresr  8058  axcnre  8100  axpre-suploclemres  8120  0re  8178  renepnf  8226  renemnf  8227  ltxrlt  8244  eqlei2  8273  0cnALT  8368  sup3exmid  9136  nn1suc  9161  nnne0  9170  xnn0xr  9469  nn0nepnf  9472  elz  9480  elnn0z  9491  elz2  9550  uzind4s  9823  elnn1uz2  9840  qre  9858  elpqb  9883  xnn0lenn0nn0  10099  xsubge0  10115  xposdif  10116  xleaddadd  10121  fzsn  10300  fz1sbc  10330  elfzp12  10333  fzm1  10334  fz01or  10345  fvinim0ffz  10486  suprzubdc  10495  zsupssdc  10497  xqltnle  10526  flqidz  10545  ceilqidz  10577  modqmuladdnn0  10629  frec2uzrand  10666  frecuzrdgtcl  10673  fzfig  10691  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  monoord  10746  seq3split  10749  seqsplitg  10750  iseqf1olemqval  10761  seq3id2  10787  seqhomog  10791  1exp  10829  bcval  11010  hashennn  11041  zfz1isolem1  11103  zfz1iso  11104  seq3coll  11105  iswrdiz  11119  0wrd0  11138  lswlgt0cl  11165  ccatval1  11173  ccatval2  11174  ccatalpha  11189  ccatrcl1  11190  wrdl1s1  11206  ccats1val2  11216  wrd2ind  11303  pfxccatin12lem3  11312  pfxccatid  11321  reuccatpfxs1lem  11326  shftlem  11376  shftfibg  11380  shftfib  11383  shftfn  11384  2shfti  11391  rexuz3  11550  sqrt0rlem  11563  cau3  11675  negfi  11788  sumdc  11918  sumrbdclem  11937  summodclem2a  11941  fisumss  11952  prodrbdclem  12131  prodmodclem2a  12136  fprodssdc  12150  fprodsplit1f  12194  ef0lem  12220  odd2np1  12433  even2n  12434  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  nn0enne  12462  divalgmod  12487  uzwodc  12607  lcmgcdlem  12648  cncongr1  12674  1nprm  12685  isprm2  12688  dvdsnprmd  12696  prmdc  12701  exprmfct  12709  nprmdvds1  12711  coprm  12715  prmdiveq  12807  prm23lt5  12835  pcpre1  12864  pc2dvds  12902  pcz  12904  pcmpt  12915  qexpz  12924  4sqlem2  12961  4sqlem19  12981  ennnfonelemhom  13035  ctiunctlemudc  13057  ssnnctlemct  13066  nninfdclemcl  13068  imasaddfnlemg  13396  ismgmid  13459  isgrpid2  13622  mhmlem  13700  eqgval  13809  dvdsrcl2  14112  nzrunit  14201  lringuplu  14209  dvdsrzring  14616  znrrg  14673  mplsubgfilemm  14711  fiinopn  14727  istopon  14736  basis2  14771  eltg3  14780  tg2  14783  tgidm  14797  bastop  14798  bastop2  14807  topnex  14809  isopn3  14848  tgrest  14892  cnpval  14921  lmbr  14936  cnconst  14957  txbas  14981  uptx  14997  txdis1cn  15001  cnmpt12  15010  cnmpt22  15017  hmeocnvb  15041  xblm  15140  isxms2  15175  mopni  15205  blssioo  15276  dedekindeulemuub  15340  dedekindeulemeu  15345  dedekindicclemuub  15349  dedekindicclemeu  15354  ivthinclemlm  15357  ivthinclemum  15358  ivthreinc  15368  lgsfvalg  15733  lgsval2lem  15738  lgsdir2lem2  15757  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  gausslemma2dlem6  15795  2lgslem1b  15817  2lgs  15832  2lgsoddprmlem2  15834  2lgsoddprmlem3  15839  2sqlem2  15843  2sqlem6  15848  2sqlem7  15849  2sqlem10  15853  vtxvalg  15866  iedgvalg  15867  umgredg  15995  upgrpredgv  15996  usgredg2vlem2  16073  ushgredgedg  16076  ushgredgedgloop  16078  griedg0ssusgr  16101  uhgrspansubgrlem  16126  vtxdgfifival  16141  iswlk  16173  upgrwlkvtxedg  16214  isclwwlknx  16266  clwwlkn1loopb  16270  clwwlknonex2lem1  16287  elabgf0  16373  bj-rspgt  16382  cbvrald  16384  decidi  16391  sumdc2  16395  bdssex  16497  bj-inex  16502  bj-intnexr  16504  bj-unexg  16516  bj-d0clsepcl  16520  bj-nnelirr  16548  bj-nn0suc  16559  bj-inf2vnlem1  16565  bj-inf2vnlem2  16566  bj-inf2vnlem3  16567  bj-inf2vnlem4  16568  bj-nn0sucALT  16573  bj-findis  16574  3dom  16587  trilpolemcl  16641