Theorem eleq1 2233

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1348  ∃wex 1485   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12  2235  eleq1i  2236  eleq1d  2239  eleq1a  2242  cleqh  2270  nelneq  2271  clelsb1  2275  nfcjust  2300  cleqf  2337  nelne2  2431  neleq1  2439  rgen2a  2524  cbvralf  2689  cbvrexf  2690  cbvreu  2694  cbvrab  2728  eqvisset  2740  ceqsralt  2757  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  rspct  2827  rspc  2828  rspce  2829  rspc2gv  2846  ceqsrexv  2860  ceqsrexbv  2861  clel2  2863  elabgt  2871  elabgf  2872  elrabi  2883  elrabf  2884  elrab3t  2885  ralab2  2894  rexab2  2896  mo2icl  2909  morex  2914  reu2  2918  reu6  2919  rmo4  2923  reu8  2926  reuind  2935  nelrdva  2937  ru  2954  dfsbcq  2957  dfsbcq2  2958  sbc8g  2962  sbcel1v  3017  rmob  3047  difjust  3122  unjust  3124  injust  3126  eldif  3130  dfss2f  3138  uniiunlem  3236  elun  3268  elin  3310  rabn0m  3442  disjne  3468  r19.3rm  3503  r19.9rmv  3506  raaanlem  3520  raaan  3521  ifmdc  3565  elpwg  3574  elpr2  3605  elsn2g  3616  rabsn  3650  tpid3g  3698  snssg  3716  difsn  3717  sssnm  3741  opeq1  3765  opeq2  3766  eluni  3799  elunii  3801  eluniab  3808  elint  3837  elintg  3839  elintab  3842  elintrabg  3844  intss1  3846  eliun  3877  eliin  3878  dfiunv2  3909  opabss  4053  cbvmpt  4084  trel  4094  trss  4096  ssex  4126  intnexr  4137  intexabim  4138  exmidel  4191  euabex  4210  elopab  4243  opelopab2a  4250  frirrg  4335  tz7.2  4339  ordelord  4366  onm  4386  ralxfr2d  4449  rexxfr2d  4450  rabxfrd  4454  reuhypd  4456  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  ontr2exmid  4509  onsucsssucexmid  4511  onsucelsucexmid  4514  ordsucunielexmid  4515  regexmidlem1  4517  elirr  4525  nordeq  4528  sucprcreg  4533  en2lp  4538  ordsoexmid  4546  ordsuc  4547  onsucuni2  4548  tfis  4567  peano2  4579  findes  4587  limom  4598  opelxp  4641  opeliunxp  4666  opbrop  4690  ssrel  4699  ssrel2  4701  ssrelrel  4711  relopabi  4737  eliunxp  4750  opeliunxp2  4751  ideqg  4762  dmmrnm  4830  dmxpm  4831  elreldm  4837  elrnmptg  4863  elres  4927  resiexg  4936  dfres2  4943  imai  4967  elimasng  4979  issref  4993  xpmlem  5031  xpm  5032  elxp4  5098  elxp5  5099  unielrel  5138  relcnvexb  5150  dmfex  5387  funfveu  5509  funimass4  5547  fvelimab  5552  ssimaex  5557  fvopab3g  5569  fvopab3ig  5570  fvmptssdm  5580  chfnrn  5607  fvelrn  5627  fmpt  5646  ffnfv  5654  fmptco  5662  elunirn  5745  f1elima  5752  cbvriota  5819  acexmidlemab  5847  acexmidlemcase  5848  cbvmpox  5931  eloprabga  5940  resoprab  5949  elrnmpo  5966  ov  5972  ovig  5974  ov6g  5990  ovg  5991  ovelrn  6001  caovimo  6046  fo1stresm  6140  fo2ndresm  6141  elxp6  6148  unielxp  6153  eqop2  6157  dfoprab4  6171  dfoprab4f  6172  fmpox  6179  1stconst  6200  2ndconst  6201  f1o2ndf1  6207  xporderlem  6210  f1od2  6214  disjxp1  6215  opeliunxp2f  6217  dftpos3  6241  dftpos4  6242  tpostpos  6243  smoel  6279  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfrcl  6343  frecabcl  6378  frecsuc  6386  nntri3or  6472  nntri3  6476  nndcel  6479  riinerm  6586  th3qlem1  6615  mapsncnv  6673  elixpsn  6713  dom2lem  6750  fiprc  6793  xpsnen  6799  phplem3g  6834  phpelm  6844  ssfiexmid  6854  domfiexmid  6856  inffiexmid  6884  undifdcss  6900  snon0  6913  f1dmvrnfibi  6921  f1vrnfibi  6922  ordiso2  7012  ctssdclemn0  7087  ctssdc  7090  enumct  7092  nnnninf  7102  nnnninfeq  7104  nninfisollemne  7107  nninfisol  7109  finomni  7116  exmidlpo  7119  acfun  7184  exmidontriimlem3  7200  exmidontriimlem4  7201  pw1ne1  7206  onntri35  7214  ccfunen  7226  cc2lem  7228  elni2  7276  recexnq  7352  recmulnqg  7353  enq0enq  7393  enq0sym  7394  enq0ref  7395  enq0tr  7396  enq0breq  7398  nqnq0pi  7400  nqnq0  7403  prop  7437  prcdnql  7446  prcunqu  7447  prubl  7448  prltlu  7449  prnmaxl  7450  prnminu  7451  prdisj  7454  prarloc  7465  genipv  7471  genpelvl  7474  genpelvu  7475  genprndl  7483  genprndu  7484  distrlem5prl  7548  distrlem5pru  7549  ltexprlemm  7562  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  aptiprleml  7601  aptiprlemu  7602  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemladdfu  7616  cauappcvgprlemladdfl  7617  caucvgprlemm  7630  caucvgprlemladdfu  7639  caucvgprprlemmu  7657  elreal2  7792  ltresr  7801  axcnre  7843  axpre-suploclemres  7863  0re  7920  renepnf  7967  renemnf  7968  ltxrlt  7985  eqlei2  8014  0cnALT  8109  sup3exmid  8873  nn1suc  8897  nnne0  8906  xnn0xr  9203  nn0nepnf  9206  elz  9214  elnn0z  9225  elz2  9283  uzind4s  9549  elnn1uz2  9566  qre  9584  elpqb  9608  xnn0lenn0nn0  9822  xsubge0  9838  xposdif  9839  xleaddadd  9844  fzsn  10022  fz1sbc  10052  elfzp12  10055  fzm1  10056  fz01or  10067  fvinim0ffz  10197  flqidz  10242  ceilqidz  10272  modqmuladdnn0  10324  frec2uzrand  10361  frecuzrdgtcl  10368  fzfig  10386  seq3fveq2  10425  seq3shft2  10429  monoord  10432  seq3split  10435  iseqf1olemqval  10443  seq3id2  10465  1exp  10505  bcval  10683  hashennn  10714  zfz1isolem1  10775  zfz1iso  10776  seq3coll  10777  shftlem  10780  shftfibg  10784  shftfib  10787  shftfn  10788  2shfti  10795  rexuz3  10954  sqrt0rlem  10967  cau3  11079  negfi  11191  sumdc  11321  sumrbdclem  11340  summodclem2a  11344  fisumss  11355  prodrbdclem  11534  prodmodclem2a  11539  fprodssdc  11553  fprodsplit1f  11597  ef0lem  11623  odd2np1  11832  even2n  11833  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  nn0enne  11861  divalgmod  11886  suprzubdc  11907  zsupssdc  11909  uzwodc  11992  lcmgcdlem  12031  cncongr1  12057  1nprm  12068  isprm2  12071  dvdsnprmd  12079  prmdc  12084  exprmfct  12092  nprmdvds1  12094  coprm  12098  prmdiveq  12190  prm23lt5  12217  pcpre1  12246  pc2dvds  12283  pcz  12285  pcmpt  12295  qexpz  12304  4sqlem2  12341  ennnfonelemhom  12370  ctiunctlemudc  12392  ssnnctlemct  12401  ismgmid  12631  isgrpid2  12743  fiinopn  12796  istopon  12805  basis2  12840  eltg3  12851  tg2  12854  tgidm  12868  bastop  12869  bastop2  12878  topnex  12880  isopn3  12919  tgrest  12963  cnpval  12992  lmbr  13007  cnconst  13028  txbas  13052  uptx  13068  txdis1cn  13072  cnmpt12  13081  cnmpt22  13088  hmeocnvb  13112  xblm  13211  isxms2  13246  mopni  13276  blssioo  13339  dedekindeulemuub  13389  dedekindeulemeu  13394  dedekindicclemuub  13398  dedekindicclemeu  13403  ivthinclemlm  13406  ivthinclemum  13407  lgsfvalg  13700  lgsval2lem  13705  lgsdir2lem2  13724  2sqlem2  13745  2sqlem6  13750  2sqlem7  13751  2sqlem10  13755  elabgf0  13812  bj-rspgt  13821  cbvrald  13823  decidi  13830  sumdc2  13834  bdssex  13937  bj-inex  13942  bj-intnexr  13944  bj-unexg  13956  bj-d0clsepcl  13960  bj-nnelirr  13988  bj-nn0suc  13999  bj-inf2vnlem1  14005  bj-inf2vnlem2  14006  bj-inf2vnlem3  14007  bj-inf2vnlem4  14008  bj-nn0sucALT  14013  bj-findis  14014  trilpolemcl  14069