Theorem eleq1 2229

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 2175	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 461	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1813	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2161	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2161	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1343  ∃wex 1480   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12  2231  eleq1i  2232  eleq1d  2235  eleq1a  2238  cleqh  2266  nelneq  2267  clelsb1  2271  nfcjust  2296  cleqf  2333  nelne2  2427  neleq1  2435  rgen2a  2520  cbvralf  2685  cbvrexf  2686  cbvreu  2690  cbvrab  2724  eqvisset  2736  ceqsralt  2753  vtoclgaf  2791  vtocl2gaf  2793  vtocl3gaf  2795  rspct  2823  rspc  2824  rspce  2825  rspc2gv  2842  ceqsrexv  2856  ceqsrexbv  2857  clel2  2859  elabgt  2867  elabgf  2868  elrabi  2879  elrabf  2880  elrab3t  2881  ralab2  2890  rexab2  2892  mo2icl  2905  morex  2910  reu2  2914  reu6  2915  rmo4  2919  reu8  2922  reuind  2931  nelrdva  2933  ru  2950  dfsbcq  2953  dfsbcq2  2954  sbc8g  2958  sbcel1v  3013  rmob  3043  difjust  3117  unjust  3119  injust  3121  eldif  3125  dfss2f  3133  uniiunlem  3231  elun  3263  elin  3305  rabn0m  3436  disjne  3462  r19.3rm  3497  r19.9rmv  3500  raaanlem  3514  raaan  3515  ifmdc  3558  elpwg  3567  elpr2  3598  elsn2g  3609  rabsn  3643  tpid3g  3691  snssg  3709  difsn  3710  sssnm  3734  opeq1  3758  opeq2  3759  eluni  3792  elunii  3794  eluniab  3801  elint  3830  elintg  3832  elintab  3835  elintrabg  3837  intss1  3839  eliun  3870  eliin  3871  dfiunv2  3902  opabss  4046  cbvmpt  4077  trel  4087  trss  4089  ssex  4119  intnexr  4130  intexabim  4131  exmidel  4184  euabex  4203  elopab  4236  opelopab2a  4243  frirrg  4328  tz7.2  4332  ordelord  4359  onm  4379  ralxfr2d  4442  rexxfr2d  4443  rabxfrd  4447  reuhypd  4449  ordtriexmid  4498  ontriexmidim  4499  ordtri2orexmid  4500  ontr2exmid  4502  onsucsssucexmid  4504  onsucelsucexmid  4507  ordsucunielexmid  4508  regexmidlem1  4510  elirr  4518  nordeq  4521  sucprcreg  4526  en2lp  4531  ordsoexmid  4539  ordsuc  4540  onsucuni2  4541  tfis  4560  peano2  4572  findes  4580  limom  4591  opelxp  4634  opeliunxp  4659  opbrop  4683  ssrel  4692  ssrel2  4694  ssrelrel  4704  relopabi  4730  eliunxp  4743  opeliunxp2  4744  ideqg  4755  dmmrnm  4823  dmxpm  4824  elreldm  4830  elrnmptg  4856  elres  4920  resiexg  4929  dfres2  4936  imai  4960  elimasng  4972  issref  4986  xpmlem  5024  xpm  5025  elxp4  5091  elxp5  5092  unielrel  5131  relcnvexb  5143  dmfex  5377  funfveu  5499  funimass4  5537  fvelimab  5542  ssimaex  5547  fvopab3g  5559  fvopab3ig  5560  fvmptssdm  5570  chfnrn  5596  fvelrn  5616  fmpt  5635  ffnfv  5643  fmptco  5651  elunirn  5734  f1elima  5741  cbvriota  5808  acexmidlemab  5836  acexmidlemcase  5837  cbvmpox  5920  eloprabga  5929  resoprab  5938  elrnmpo  5955  ov  5961  ovig  5963  ov6g  5979  ovg  5980  ovelrn  5990  caovimo  6035  fo1stresm  6129  fo2ndresm  6130  elxp6  6137  unielxp  6142  eqop2  6146  dfoprab4  6160  dfoprab4f  6161  fmpox  6168  1stconst  6189  2ndconst  6190  f1o2ndf1  6196  xporderlem  6199  f1od2  6203  disjxp1  6204  opeliunxp2f  6206  dftpos3  6230  dftpos4  6231  tpostpos  6232  smoel  6268  tfr1onlemaccex  6316  tfrcllemaccex  6329  tfrcl  6332  frecabcl  6367  frecsuc  6375  nntri3or  6461  nntri3  6465  nndcel  6468  riinerm  6574  th3qlem1  6603  mapsncnv  6661  elixpsn  6701  dom2lem  6738  fiprc  6781  xpsnen  6787  phplem3g  6822  phpelm  6832  ssfiexmid  6842  domfiexmid  6844  inffiexmid  6872  undifdcss  6888  snon0  6901  f1dmvrnfibi  6909  f1vrnfibi  6910  ordiso2  7000  ctssdclemn0  7075  ctssdc  7078  enumct  7080  nnnninf  7090  nnnninfeq  7092  nninfisollemne  7095  nninfisol  7097  finomni  7104  exmidlpo  7107  acfun  7163  exmidontriimlem3  7179  exmidontriimlem4  7180  pw1ne1  7185  onntri35  7193  ccfunen  7205  cc2lem  7207  elni2  7255  recexnq  7331  recmulnqg  7332  enq0enq  7372  enq0sym  7373  enq0ref  7374  enq0tr  7375  enq0breq  7377  nqnq0pi  7379  nqnq0  7382  prop  7416  prcdnql  7425  prcunqu  7426  prubl  7427  prltlu  7428  prnmaxl  7429  prnminu  7430  prdisj  7433  prarloc  7444  genipv  7450  genpelvl  7453  genpelvu  7454  genprndl  7462  genprndu  7463  distrlem5prl  7527  distrlem5pru  7528  ltexprlemm  7541  ltexprlemdisj  7547  ltexprlemloc  7548  ltexprlemrl  7551  ltexprlemru  7553  aptiprleml  7580  aptiprlemu  7581  archpr  7584  cauappcvgprlemm  7586  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  caucvgprlemm  7609  caucvgprlemladdfu  7618  caucvgprprlemmu  7636  elreal2  7771  ltresr  7780  axcnre  7822  axpre-suploclemres  7842  0re  7899  renepnf  7946  renemnf  7947  ltxrlt  7964  eqlei2  7993  0cnALT  8088  sup3exmid  8852  nn1suc  8876  nnne0  8885  xnn0xr  9182  nn0nepnf  9185  elz  9193  elnn0z  9204  elz2  9262  uzind4s  9528  elnn1uz2  9545  qre  9563  elpqb  9587  xnn0lenn0nn0  9801  xsubge0  9817  xposdif  9818  xleaddadd  9823  fzsn  10001  fz1sbc  10031  elfzp12  10034  fzm1  10035  fz01or  10046  fvinim0ffz  10176  flqidz  10221  ceilqidz  10251  modqmuladdnn0  10303  frec2uzrand  10340  frecuzrdgtcl  10347  fzfig  10365  seq3fveq2  10404  seq3shft2  10408  monoord  10411  seq3split  10414  iseqf1olemqval  10422  seq3id2  10444  1exp  10484  bcval  10662  hashennn  10693  zfz1isolem1  10753  zfz1iso  10754  seq3coll  10755  shftlem  10758  shftfibg  10762  shftfib  10765  shftfn  10766  2shfti  10773  rexuz3  10932  sqrt0rlem  10945  cau3  11057  negfi  11169  sumdc  11299  sumrbdclem  11318  summodclem2a  11322  fisumss  11333  prodrbdclem  11512  prodmodclem2a  11517  fprodssdc  11531  fprodsplit1f  11575  ef0lem  11601  odd2np1  11810  even2n  11811  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  nn0enne  11839  divalgmod  11864  suprzubdc  11885  zsupssdc  11887  uzwodc  11970  lcmgcdlem  12009  cncongr1  12035  1nprm  12046  isprm2  12049  dvdsnprmd  12057  prmdc  12062  exprmfct  12070  nprmdvds1  12072  coprm  12076  prmdiveq  12168  prm23lt5  12195  pcpre1  12224  pc2dvds  12261  pcz  12263  pcmpt  12273  qexpz  12282  4sqlem2  12319  ennnfonelemhom  12348  ctiunctlemudc  12370  ssnnctlemct  12379  ismgmid  12608  fiinopn  12642  istopon  12651  basis2  12686  eltg3  12697  tg2  12700  tgidm  12714  bastop  12715  bastop2  12724  topnex  12726  isopn3  12765  tgrest  12809  cnpval  12838  lmbr  12853  cnconst  12874  txbas  12898  uptx  12914  txdis1cn  12918  cnmpt12  12927  cnmpt22  12934  hmeocnvb  12958  xblm  13057  isxms2  13092  mopni  13122  blssioo  13185  dedekindeulemuub  13235  dedekindeulemeu  13240  dedekindicclemuub  13244  dedekindicclemeu  13249  ivthinclemlm  13252  ivthinclemum  13253  lgsfvalg  13546  lgsval2lem  13551  lgsdir2lem2  13570  2sqlem2  13591  2sqlem6  13596  2sqlem7  13597  2sqlem10  13601  elabgf0  13658  bj-rspgt  13667  cbvrald  13669  decidi  13676  sumdc2  13680  bdssex  13784  bj-inex  13789  bj-intnexr  13791  bj-unexg  13803  bj-d0clsepcl  13807  bj-nnelirr  13835  bj-nn0suc  13846  bj-inf2vnlem1  13852  bj-inf2vnlem2  13853  bj-inf2vnlem3  13854  bj-inf2vnlem4  13855  bj-nn0sucALT  13860  bj-findis  13861  trilpolemcl  13916