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  4303  opelopab2a  4310  frirrg  4396  tz7.2  4400  ordelord  4427  onm  4447  ralxfr2d  4510  rexxfr2d  4511  rabxfrd  4515  reuhypd  4517  ordtriexmid  4568  ontriexmidim  4569  ordtri2orexmid  4570  ontr2exmid  4572  onsucsssucexmid  4574  onsucelsucexmid  4577  ordsucunielexmid  4578  regexmidlem1  4580  elirr  4588  nordeq  4591  sucprcreg  4596  en2lp  4601  ordsoexmid  4609  ordsuc  4610  onsucuni2  4611  tfis  4630  peano2  4642  findes  4650  limom  4661  opelxp  4704  opeliunxp  4729  opbrop  4753  ssrel  4762  ssrel2  4764  ssrelrel  4774  relopabi  4802  eliunxp  4816  opeliunxp2  4817  ideqg  4828  dmmrnm  4896  dmxpm  4897  elreldm  4903  elrnmptg  4929  elres  4994  resiexg  5003  dfres2  5010  imai  5037  elimasng  5049  issref  5064  xpmlem  5102  xpm  5103  elxp4  5169  elxp5  5170  unielrel  5209  relcnvexb  5221  dmfex  5464  funfveu  5588  funimass4  5628  fvelimab  5634  ssimaex  5639  fvopab3g  5651  fvopab3ig  5652  fvmptssdm  5663  chfnrn  5690  fvelrn  5710  fmpt  5729  ffnfv  5737  fmptco  5745  elunirn  5834  f1elima  5841  cbvriota  5909  acexmidlemab  5937  acexmidlemcase  5938  cbvmpox  6022  eloprabga  6031  resoprab  6040  elrnmpo  6058  ov  6064  ovig  6066  ov6g  6083  ovg  6084  ovelrn  6094  caovimo  6139  fo1stresm  6246  fo2ndresm  6247  elxp6  6254  unielxp  6259  eqop2  6263  dfoprab4  6277  dfoprab4f  6278  fmpox  6285  1stconst  6306  2ndconst  6307  f1o2ndf1  6313  xporderlem  6316  f1od2  6320  disjxp1  6321  opeliunxp2f  6323  dftpos3  6347  dftpos4  6348  tpostpos  6349  smoel  6385  tfr1onlemaccex  6433  tfrcllemaccex  6446  tfrcl  6449  frecabcl  6484  frecsuc  6492  nntri3or  6578  nntri3  6582  nndcel  6585  riinerm  6694  th3qlem1  6723  mapsncnv  6781  elixpsn  6821  dom2lem  6862  fiprc  6906  xpsnen  6915  phplem3g  6952  phpelm  6962  ssfiexmid  6972  domfiexmid  6974  inffiexmid  7002  undifdcss  7019  opabfi  7034  snon0  7036  f1dmvrnfibi  7045  f1vrnfibi  7046  ordiso2  7136  ctssdclemn0  7211  ctssdc  7214  enumct  7216  nnnninf  7227  nnnninfeq  7229  nninfisollemne  7232  nninfisol  7234  finomni  7241  exmidlpo  7244  acneq  7313  finacn  7315  acfun  7318  exmidontriimlem3  7334  exmidontriimlem4  7335  pw1ne1  7340  onntri35  7348  exmidapne  7371  ccfunen  7375  cc2lem  7377  elni2  7426  recexnq  7502  recmulnqg  7503  enq0enq  7543  enq0sym  7544  enq0ref  7545  enq0tr  7546  enq0breq  7548  nqnq0pi  7550  nqnq0  7553  prop  7587  prcdnql  7596  prcunqu  7597  prubl  7598  prltlu  7599  prnmaxl  7600  prnminu  7601  prdisj  7604  prarloc  7615  genipv  7621  genpelvl  7624  genpelvu  7625  genprndl  7633  genprndu  7634  distrlem5prl  7698  distrlem5pru  7699  ltexprlemm  7712  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemrl  7722  ltexprlemru  7724  aptiprleml  7751  aptiprlemu  7752  archpr  7755  cauappcvgprlemm  7757  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  caucvgprlemm  7780  caucvgprlemladdfu  7789  caucvgprprlemmu  7807  elreal2  7942  ltresr  7951  axcnre  7993  axpre-suploclemres  8013  0re  8071  renepnf  8119  renemnf  8120  ltxrlt  8137  eqlei2  8166  0cnALT  8261  sup3exmid  9029  nn1suc  9054  nnne0  9063  xnn0xr  9362  nn0nepnf  9365  elz  9373  elnn0z  9384  elz2  9443  uzind4s  9710  elnn1uz2  9727  qre  9745  elpqb  9770  xnn0lenn0nn0  9986  xsubge0  10002  xposdif  10003  xleaddadd  10008  fzsn  10187  fz1sbc  10217  elfzp12  10220  fzm1  10221  fz01or  10232  fvinim0ffz  10368  suprzubdc  10377  zsupssdc  10379  xqltnle  10408  flqidz  10427  ceilqidz  10459  modqmuladdnn0  10511  frec2uzrand  10548  frecuzrdgtcl  10555  fzfig  10573  seq3fveq2  10618  seqfveq2g  10620  seq3shft2  10624  seqshft2g  10625  monoord  10628  seq3split  10631  seqsplitg  10632  iseqf1olemqval  10643  seq3id2  10669  seqhomog  10673  1exp  10711  bcval  10892  hashennn  10923  zfz1isolem1  10983  zfz1iso  10984  seq3coll  10985  iswrdiz  10999  0wrd0  11018  lswlgt0cl  11043  ccatval1  11051  ccatval2  11052  wrdl1s1  11082  ccats1val2  11090  shftlem  11098  shftfibg  11102  shftfib  11105  shftfn  11106  2shfti  11113  rexuz3  11272  sqrt0rlem  11285  cau3  11397  negfi  11510  sumdc  11640  sumrbdclem  11659  summodclem2a  11663  fisumss  11674  prodrbdclem  11853  prodmodclem2a  11858  fprodssdc  11872  fprodsplit1f  11916  ef0lem  11942  odd2np1  12155  even2n  12156  oddnn02np1  12162  oddge22np1  12163  evennn02n  12164  evennn2n  12165  nn0enne  12184  divalgmod  12209  uzwodc  12329  lcmgcdlem  12370  cncongr1  12396  1nprm  12407  isprm2  12410  dvdsnprmd  12418  prmdc  12423  exprmfct  12431  nprmdvds1  12433  coprm  12437  prmdiveq  12529  prm23lt5  12557  pcpre1  12586  pc2dvds  12624  pcz  12626  pcmpt  12637  qexpz  12646  4sqlem2  12683  4sqlem19  12703  ennnfonelemhom  12757  ctiunctlemudc  12779  ssnnctlemct  12788  nninfdclemcl  12790  imasaddfnlemg  13117  ismgmid  13180  isgrpid2  13343  mhmlem  13421  eqgval  13530  dvdsrcl2  13832  nzrunit  13921  lringuplu  13929  dvdsrzring  14336  znrrg  14393  mplsubgfilemm  14431  fiinopn  14447  istopon  14456  basis2  14491  eltg3  14500  tg2  14503  tgidm  14517  bastop  14518  bastop2  14527  topnex  14529  isopn3  14568  tgrest  14612  cnpval  14641  lmbr  14656  cnconst  14677  txbas  14701  uptx  14717  txdis1cn  14721  cnmpt12  14730  cnmpt22  14737  hmeocnvb  14761  xblm  14860  isxms2  14895  mopni  14925  blssioo  14996  dedekindeulemuub  15060  dedekindeulemeu  15065  dedekindicclemuub  15069  dedekindicclemeu  15074  ivthinclemlm  15077  ivthinclemum  15078  ivthreinc  15088  lgsfvalg  15453  lgsval2lem  15458  lgsdir2lem2  15477  gausslemma2dlem1a  15506  gausslemma2dlem4  15512  gausslemma2dlem6  15515  2lgslem1b  15537  2lgs  15552  2lgsoddprmlem2  15554  2lgsoddprmlem3  15559  2sqlem2  15563  2sqlem6  15568  2sqlem7  15569  2sqlem10  15573  vtxvalg  15586  iedgvalg  15587  elabgf0  15675  bj-rspgt  15684  cbvrald  15686  decidi  15693  sumdc2  15697  bdssex  15800  bj-inex  15805  bj-intnexr  15807  bj-unexg  15819  bj-d0clsepcl  15823  bj-nnelirr  15851  bj-nn0suc  15862  bj-inf2vnlem1  15868  bj-inf2vnlem2  15869  bj-inf2vnlem3  15870  bj-inf2vnlem4  15871  bj-nn0sucALT  15876  bj-findis  15877  trilpolemcl  15938