Theorem eleq1 2292

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395  ∃wex 1538   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq1i  2295  eleq1d  2298  eleq1a  2301  cleqh  2329  nelneq  2330  clelsb1  2334  nfcjust  2360  cleqf  2397  nelne2  2491  neleq1  2499  rgen2a  2584  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  eqvisset  2810  ceqsralt  2827  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspce  2902  rspc2gv  2919  ceqsrexv  2933  ceqsrexbv  2934  clel2  2936  elabgt  2944  elabgf  2945  elrabi  2956  elrabf  2957  elrab3t  2958  ralab2  2967  rexab2  2969  mo2icl  2982  morex  2987  reu2  2991  reu6  2992  rmo4  2996  reu8  2999  reuind  3008  nelrdva  3010  ru  3027  dfsbcq  3030  dfsbcq2  3031  sbc8g  3036  sbcel1v  3091  rmob  3122  difjust  3198  unjust  3200  injust  3202  eldif  3206  dfss2f  3215  uniiunlem  3313  elun  3345  elin  3387  rabn0m  3519  disjne  3545  r19.3rm  3580  r19.9rmv  3583  raaanlem  3596  raaan  3597  elif  3614  ifmdc  3645  elpwg  3657  elpr2  3688  elsn2g  3699  rabsn  3733  tpid3g  3782  snssb  3801  snssgOLD  3804  difsn  3805  sssnm  3832  opeq1  3857  opeq2  3858  eluni  3891  elunii  3893  eluniab  3900  elint  3929  elintg  3931  elintab  3934  elintrabg  3936  intss1  3938  eliun  3969  eliin  3970  dfiunv2  4001  opabss  4148  cbvmpt  4179  trel  4189  trss  4191  ssex  4221  intnexr  4235  intexabim  4236  exmidel  4289  euabex  4311  elopab  4346  opelopab2a  4353  frirrg  4441  tz7.2  4445  ordelord  4472  onm  4492  ralxfr2d  4555  rexxfr2d  4556  rabxfrd  4560  reuhypd  4562  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  ordsucunielexmid  4623  regexmidlem1  4625  elirr  4633  nordeq  4636  sucprcreg  4641  en2lp  4646  ordsoexmid  4654  ordsuc  4655  onsucuni2  4656  tfis  4675  peano2  4687  findes  4695  limom  4706  opelxp  4749  opeliunxp  4774  opbrop  4798  ssrel  4807  ssrel2  4809  ssrelrel  4819  relopabi  4847  eliunxp  4861  opeliunxp2  4862  ideqg  4873  reldmm  4942  dmmrnm  4943  dmxpm  4944  elreldm  4950  elrnmptg  4976  elres  5041  resiexg  5050  dfres2  5057  imai  5084  elimasng  5096  issref  5111  xpmlem  5149  xpm  5150  elxp4  5216  elxp5  5217  unielrel  5256  relcnvexb  5268  dmfex  5517  funfveu  5642  funimass4  5686  fvelimab  5692  ssimaex  5697  fvopab3g  5709  fvopab3ig  5710  fvmptssdm  5721  chfnrn  5748  fvelrn  5768  fmpt  5787  ffnfv  5795  fmptco  5803  elunirn  5896  f1elima  5903  cbvriota  5972  acexmidlemab  6001  acexmidlemcase  6002  cbvmpox  6088  eloprabga  6097  resoprab  6106  elrnmpo  6124  ov  6130  ovig  6132  ov6g  6149  ovg  6150  ovelrn  6160  caovimo  6205  fo1stresm  6313  fo2ndresm  6314  elxp6  6321  unielxp  6326  eqop2  6330  dfoprab4  6344  dfoprab4f  6345  fmpox  6352  1stconst  6373  2ndconst  6374  f1o2ndf1  6380  xporderlem  6383  f1od2  6387  disjxp1  6388  opeliunxp2f  6390  dftpos3  6414  dftpos4  6415  tpostpos  6416  smoel  6452  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcl  6516  frecabcl  6551  frecsuc  6559  nntri3or  6647  nntri3  6651  nndcel  6654  riinerm  6763  th3qlem1  6792  mapsncnv  6850  elixpsn  6890  dom2lem  6931  fiprc  6976  xpsnen  6988  phplem3g  7025  phpelm  7036  ssfiexmid  7046  domfiexmid  7048  elssdc  7075  inffiexmid  7079  undifdcss  7096  opabfi  7111  snon0  7113  f1dmvrnfibi  7122  f1vrnfibi  7123  ordiso2  7213  ctssdclemn0  7288  ctssdc  7291  enumct  7293  nnnninf  7304  nnnninfeq  7306  nninfisollemne  7309  nninfisol  7311  finomni  7318  exmidlpo  7321  pr2cv1  7379  acneq  7395  finacn  7397  acfun  7400  exmidontriimlem3  7416  exmidontriimlem4  7417  pw1ne1  7425  onntri35  7433  exmidapne  7457  ccfunen  7461  cc2lem  7463  elni2  7512  recexnq  7588  recmulnqg  7589  enq0enq  7629  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  nqnq0pi  7636  nqnq0  7639  prop  7673  prcdnql  7682  prcunqu  7683  prubl  7684  prltlu  7685  prnmaxl  7686  prnminu  7687  prdisj  7690  prarloc  7701  genipv  7707  genpelvl  7710  genpelvu  7711  genprndl  7719  genprndu  7720  distrlem5prl  7784  distrlem5pru  7785  ltexprlemm  7798  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  aptiprleml  7837  aptiprlemu  7838  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemm  7866  caucvgprlemladdfu  7875  caucvgprprlemmu  7893  elreal2  8028  ltresr  8037  axcnre  8079  axpre-suploclemres  8099  0re  8157  renepnf  8205  renemnf  8206  ltxrlt  8223  eqlei2  8252  0cnALT  8347  sup3exmid  9115  nn1suc  9140  nnne0  9149  xnn0xr  9448  nn0nepnf  9451  elz  9459  elnn0z  9470  elz2  9529  uzind4s  9797  elnn1uz2  9814  qre  9832  elpqb  9857  xnn0lenn0nn0  10073  xsubge0  10089  xposdif  10090  xleaddadd  10095  fzsn  10274  fz1sbc  10304  elfzp12  10307  fzm1  10308  fz01or  10319  fvinim0ffz  10459  suprzubdc  10468  zsupssdc  10470  xqltnle  10499  flqidz  10518  ceilqidz  10550  modqmuladdnn0  10602  frec2uzrand  10639  frecuzrdgtcl  10646  fzfig  10664  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  monoord  10719  seq3split  10722  seqsplitg  10723  iseqf1olemqval  10734  seq3id2  10760  seqhomog  10764  1exp  10802  bcval  10983  hashennn  11014  zfz1isolem1  11075  zfz1iso  11076  seq3coll  11077  iswrdiz  11091  0wrd0  11110  lswlgt0cl  11137  ccatval1  11145  ccatval2  11146  ccatalpha  11161  ccatrcl1  11162  wrdl1s1  11178  ccats1val2  11186  wrd2ind  11270  pfxccatin12lem3  11279  pfxccatid  11288  reuccatpfxs1lem  11293  shftlem  11342  shftfibg  11346  shftfib  11349  shftfn  11350  2shfti  11357  rexuz3  11516  sqrt0rlem  11529  cau3  11641  negfi  11754  sumdc  11884  sumrbdclem  11903  summodclem2a  11907  fisumss  11918  prodrbdclem  12097  prodmodclem2a  12102  fprodssdc  12116  fprodsplit1f  12160  ef0lem  12186  odd2np1  12399  even2n  12400  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  nn0enne  12428  divalgmod  12453  uzwodc  12573  lcmgcdlem  12614  cncongr1  12640  1nprm  12651  isprm2  12654  dvdsnprmd  12662  prmdc  12667  exprmfct  12675  nprmdvds1  12677  coprm  12681  prmdiveq  12773  prm23lt5  12801  pcpre1  12830  pc2dvds  12868  pcz  12870  pcmpt  12881  qexpz  12890  4sqlem2  12927  4sqlem19  12947  ennnfonelemhom  13001  ctiunctlemudc  13023  ssnnctlemct  13032  nninfdclemcl  13034  imasaddfnlemg  13362  ismgmid  13425  isgrpid2  13588  mhmlem  13666  eqgval  13775  dvdsrcl2  14078  nzrunit  14167  lringuplu  14175  dvdsrzring  14582  znrrg  14639  mplsubgfilemm  14677  fiinopn  14693  istopon  14702  basis2  14737  eltg3  14746  tg2  14749  tgidm  14763  bastop  14764  bastop2  14773  topnex  14775  isopn3  14814  tgrest  14858  cnpval  14887  lmbr  14902  cnconst  14923  txbas  14947  uptx  14963  txdis1cn  14967  cnmpt12  14976  cnmpt22  14983  hmeocnvb  15007  xblm  15106  isxms2  15141  mopni  15171  blssioo  15242  dedekindeulemuub  15306  dedekindeulemeu  15311  dedekindicclemuub  15315  dedekindicclemeu  15320  ivthinclemlm  15323  ivthinclemum  15324  ivthreinc  15334  lgsfvalg  15699  lgsval2lem  15704  lgsdir2lem2  15723  gausslemma2dlem1a  15752  gausslemma2dlem4  15758  gausslemma2dlem6  15761  2lgslem1b  15783  2lgs  15798  2lgsoddprmlem2  15800  2lgsoddprmlem3  15805  2sqlem2  15809  2sqlem6  15814  2sqlem7  15815  2sqlem10  15819  vtxvalg  15832  iedgvalg  15833  umgredg  15958  upgrpredgv  15959  usgredg2vlem2  16036  ushgredgedg  16039  ushgredgedgloop  16041  vtxdgfifival  16050  iswlk  16064  upgrwlkvtxedg  16105  elabgf0  16196  bj-rspgt  16205  cbvrald  16207  decidi  16214  sumdc2  16218  bdssex  16320  bj-inex  16325  bj-intnexr  16327  bj-unexg  16339  bj-d0clsepcl  16343  bj-nnelirr  16371  bj-nn0suc  16382  bj-inf2vnlem1  16388  bj-inf2vnlem2  16389  bj-inf2vnlem3  16390  bj-inf2vnlem4  16391  bj-nn0sucALT  16396  bj-findis  16397  3dom  16411  trilpolemcl  16465