Theorem eleq1 2267

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372  ∃wex 1514   ∈ wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  eleq12  2269  eleq1i  2270  eleq1d  2273  eleq1a  2276  cleqh  2304  nelneq  2305  clelsb1  2309  nfcjust  2335  cleqf  2372  nelne2  2466  neleq1  2474  rgen2a  2559  cbvralf  2729  cbvrexf  2730  cbvreu  2735  cbvrab  2769  eqvisset  2781  ceqsralt  2798  vtoclgaf  2837  vtocl2gaf  2839  vtocl3gaf  2841  rspct  2869  rspc  2870  rspce  2871  rspc2gv  2888  ceqsrexv  2902  ceqsrexbv  2903  clel2  2905  elabgt  2913  elabgf  2914  elrabi  2925  elrabf  2926  elrab3t  2927  ralab2  2936  rexab2  2938  mo2icl  2951  morex  2956  reu2  2960  reu6  2961  rmo4  2965  reu8  2968  reuind  2977  nelrdva  2979  ru  2996  dfsbcq  2999  dfsbcq2  3000  sbc8g  3005  sbcel1v  3060  rmob  3090  difjust  3166  unjust  3168  injust  3170  eldif  3174  dfss2f  3183  uniiunlem  3281  elun  3313  elin  3355  rabn0m  3487  disjne  3513  r19.3rm  3548  r19.9rmv  3551  raaanlem  3564  raaan  3565  ifmdc  3611  elpwg  3623  elpr2  3654  elsn2g  3665  rabsn  3699  tpid3g  3747  snssb  3765  snssgOLD  3768  difsn  3769  sssnm  3794  opeq1  3818  opeq2  3819  eluni  3852  elunii  3854  eluniab  3861  elint  3890  elintg  3892  elintab  3895  elintrabg  3897  intss1  3899  eliun  3930  eliin  3931  dfiunv2  3962  opabss  4107  cbvmpt  4138  trel  4148  trss  4150  ssex  4180  intnexr  4194  intexabim  4195  exmidel  4248  euabex  4268  elopab  4302  opelopab2a  4309  frirrg  4395  tz7.2  4399  ordelord  4426  onm  4446  ralxfr2d  4509  rexxfr2d  4510  rabxfrd  4514  reuhypd  4516  ordtriexmid  4567  ontriexmidim  4568  ordtri2orexmid  4569  ontr2exmid  4571  onsucsssucexmid  4573  onsucelsucexmid  4576  ordsucunielexmid  4577  regexmidlem1  4579  elirr  4587  nordeq  4590  sucprcreg  4595  en2lp  4600  ordsoexmid  4608  ordsuc  4609  onsucuni2  4610  tfis  4629  peano2  4641  findes  4649  limom  4660  opelxp  4703  opeliunxp  4728  opbrop  4752  ssrel  4761  ssrel2  4763  ssrelrel  4773  relopabi  4801  eliunxp  4815  opeliunxp2  4816  ideqg  4827  dmmrnm  4895  dmxpm  4896  elreldm  4902  elrnmptg  4928  elres  4992  resiexg  5001  dfres2  5008  imai  5035  elimasng  5047  issref  5062  xpmlem  5100  xpm  5101  elxp4  5167  elxp5  5168  unielrel  5207  relcnvexb  5219  dmfex  5459  funfveu  5583  funimass4  5623  fvelimab  5629  ssimaex  5634  fvopab3g  5646  fvopab3ig  5647  fvmptssdm  5658  chfnrn  5685  fvelrn  5705  fmpt  5724  ffnfv  5732  fmptco  5740  elunirn  5825  f1elima  5832  cbvriota  5900  acexmidlemab  5928  acexmidlemcase  5929  cbvmpox  6013  eloprabga  6022  resoprab  6031  elrnmpo  6049  ov  6055  ovig  6057  ov6g  6074  ovg  6075  ovelrn  6085  caovimo  6130  fo1stresm  6237  fo2ndresm  6238  elxp6  6245  unielxp  6250  eqop2  6254  dfoprab4  6268  dfoprab4f  6269  fmpox  6276  1stconst  6297  2ndconst  6298  f1o2ndf1  6304  xporderlem  6307  f1od2  6311  disjxp1  6312  opeliunxp2f  6314  dftpos3  6338  dftpos4  6339  tpostpos  6340  smoel  6376  tfr1onlemaccex  6424  tfrcllemaccex  6437  tfrcl  6440  frecabcl  6475  frecsuc  6483  nntri3or  6569  nntri3  6573  nndcel  6576  riinerm  6685  th3qlem1  6714  mapsncnv  6772  elixpsn  6812  dom2lem  6849  fiprc  6892  xpsnen  6898  phplem3g  6935  phpelm  6945  ssfiexmid  6955  domfiexmid  6957  inffiexmid  6985  undifdcss  7002  opabfi  7017  snon0  7019  f1dmvrnfibi  7028  f1vrnfibi  7029  ordiso2  7119  ctssdclemn0  7194  ctssdc  7197  enumct  7199  nnnninf  7210  nnnninfeq  7212  nninfisollemne  7215  nninfisol  7217  finomni  7224  exmidlpo  7227  acneq  7296  finacn  7298  acfun  7301  exmidontriimlem3  7317  exmidontriimlem4  7318  pw1ne1  7323  onntri35  7331  exmidapne  7354  ccfunen  7358  cc2lem  7360  elni2  7409  recexnq  7485  recmulnqg  7486  enq0enq  7526  enq0sym  7527  enq0ref  7528  enq0tr  7529  enq0breq  7531  nqnq0pi  7533  nqnq0  7536  prop  7570  prcdnql  7579  prcunqu  7580  prubl  7581  prltlu  7582  prnmaxl  7583  prnminu  7584  prdisj  7587  prarloc  7598  genipv  7604  genpelvl  7607  genpelvu  7608  genprndl  7616  genprndu  7617  distrlem5prl  7681  distrlem5pru  7682  ltexprlemm  7695  ltexprlemdisj  7701  ltexprlemloc  7702  ltexprlemrl  7705  ltexprlemru  7707  aptiprleml  7734  aptiprlemu  7735  archpr  7738  cauappcvgprlemm  7740  cauappcvgprlemladdfu  7749  cauappcvgprlemladdfl  7750  caucvgprlemm  7763  caucvgprlemladdfu  7772  caucvgprprlemmu  7790  elreal2  7925  ltresr  7934  axcnre  7976  axpre-suploclemres  7996  0re  8054  renepnf  8102  renemnf  8103  ltxrlt  8120  eqlei2  8149  0cnALT  8244  sup3exmid  9012  nn1suc  9037  nnne0  9046  xnn0xr  9345  nn0nepnf  9348  elz  9356  elnn0z  9367  elz2  9426  uzind4s  9693  elnn1uz2  9710  qre  9728  elpqb  9753  xnn0lenn0nn0  9969  xsubge0  9985  xposdif  9986  xleaddadd  9991  fzsn  10170  fz1sbc  10200  elfzp12  10203  fzm1  10204  fz01or  10215  fvinim0ffz  10351  suprzubdc  10360  zsupssdc  10362  xqltnle  10391  flqidz  10410  ceilqidz  10442  modqmuladdnn0  10494  frec2uzrand  10531  frecuzrdgtcl  10538  fzfig  10556  seq3fveq2  10601  seqfveq2g  10603  seq3shft2  10607  seqshft2g  10608  monoord  10611  seq3split  10614  seqsplitg  10615  iseqf1olemqval  10626  seq3id2  10652  seqhomog  10656  1exp  10694  bcval  10875  hashennn  10906  zfz1isolem1  10966  zfz1iso  10967  seq3coll  10968  iswrdiz  10976  0wrd0  10995  lswlgt0cl  11020  ccatval1  11028  ccatval2  11029  shftlem  11046  shftfibg  11050  shftfib  11053  shftfn  11054  2shfti  11061  rexuz3  11220  sqrt0rlem  11233  cau3  11345  negfi  11458  sumdc  11588  sumrbdclem  11607  summodclem2a  11611  fisumss  11622  prodrbdclem  11801  prodmodclem2a  11806  fprodssdc  11820  fprodsplit1f  11864  ef0lem  11890  odd2np1  12103  even2n  12104  oddnn02np1  12110  oddge22np1  12111  evennn02n  12112  evennn2n  12113  nn0enne  12132  divalgmod  12157  uzwodc  12277  lcmgcdlem  12318  cncongr1  12344  1nprm  12355  isprm2  12358  dvdsnprmd  12366  prmdc  12371  exprmfct  12379  nprmdvds1  12381  coprm  12385  prmdiveq  12477  prm23lt5  12505  pcpre1  12534  pc2dvds  12572  pcz  12574  pcmpt  12585  qexpz  12594  4sqlem2  12631  4sqlem19  12651  ennnfonelemhom  12705  ctiunctlemudc  12727  ssnnctlemct  12736  nninfdclemcl  12738  imasaddfnlemg  13064  ismgmid  13127  isgrpid2  13290  mhmlem  13368  eqgval  13477  dvdsrcl2  13779  nzrunit  13868  lringuplu  13876  dvdsrzring  14283  znrrg  14340  mplsubgfilemm  14378  fiinopn  14394  istopon  14403  basis2  14438  eltg3  14447  tg2  14450  tgidm  14464  bastop  14465  bastop2  14474  topnex  14476  isopn3  14515  tgrest  14559  cnpval  14588  lmbr  14603  cnconst  14624  txbas  14648  uptx  14664  txdis1cn  14668  cnmpt12  14677  cnmpt22  14684  hmeocnvb  14708  xblm  14807  isxms2  14842  mopni  14872  blssioo  14943  dedekindeulemuub  15007  dedekindeulemeu  15012  dedekindicclemuub  15016  dedekindicclemeu  15021  ivthinclemlm  15024  ivthinclemum  15025  ivthreinc  15035  lgsfvalg  15400  lgsval2lem  15405  lgsdir2lem2  15424  gausslemma2dlem1a  15453  gausslemma2dlem4  15459  gausslemma2dlem6  15462  2lgslem1b  15484  2lgs  15499  2lgsoddprmlem2  15501  2lgsoddprmlem3  15506  2sqlem2  15510  2sqlem6  15515  2sqlem7  15516  2sqlem10  15520  elabgf0  15577  bj-rspgt  15586  cbvrald  15588  decidi  15595  sumdc2  15599  bdssex  15702  bj-inex  15707  bj-intnexr  15709  bj-unexg  15721  bj-d0clsepcl  15725  bj-nnelirr  15753  bj-nn0suc  15764  bj-inf2vnlem1  15770  bj-inf2vnlem2  15771  bj-inf2vnlem3  15772  bj-inf2vnlem4  15773  bj-nn0sucALT  15778  bj-findis  15779  trilpolemcl  15840