Theorem eleq1 2301

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12  2303  eleq1i  2304  eleq1d  2307  eleq1a  2310  cleqh  2338  nelneq  2339  clelsb1  2343  nfcjust  2380  cleqf  2417  nelne2  2511  neleq1  2519  rgen2a  2604  cbvralf  2777  cbvrexf  2778  cbvreu  2784  cbvrab  2819  eqvisset  2832  ceqsralt  2849  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  rspce  2924  rspc2gv  2942  ceqsrexv  2956  ceqsrexbv  2957  clel2  2959  elabgt  2967  elabgf  2968  elrabi  2979  elrabf  2980  elrab3t  2981  ralab2  2990  rexab2  2992  mo2icl  3005  morex  3010  reu2  3014  reu6  3015  rmo4  3019  reu8  3022  reuind  3031  nelrdva  3033  ru  3050  dfsbcq  3053  dfsbcq2  3054  sbc8g  3059  sbcel1v  3114  rmob  3145  difjust  3221  unjust  3223  injust  3225  eldif  3229  dfssf  3238  dfss2f  3239  uniiunlem  3338  elun  3370  elin  3412  rabn0m  3549  disjne  3578  r19.3rm  3616  r19.9rmv  3619  raaanlem  3632  raaan  3633  elif  3652  ifmdc  3683  elpwg  3696  elpr2  3731  elsn2g  3742  rabsn  3776  tpid3g  3828  snssb  3848  snssgOLD  3851  difsn  3852  sssnm  3879  opeq1  3904  opeq2  3905  eluni  3938  elunii  3940  eluniab  3947  elint  3976  elintg  3978  elintab  3981  elintrabg  3983  intss1  3985  eliun  4016  eliin  4017  dfiunv2  4048  opabss  4196  cbvmpt  4228  trel  4238  trss  4240  ssex  4272  intnexr  4289  intexabim  4290  exmidel  4344  euabex  4367  elopab  4402  opelopab2a  4409  frirrg  4497  tz7.2  4501  ordelord  4528  onm  4548  ralxfr2d  4612  rexxfr2d  4613  rabxfrd  4617  reuhypd  4619  ordtriexmid  4670  ontriexmidim  4671  ordtri2orexmid  4672  ontr2exmid  4674  onsucsssucexmid  4676  onsucelsucexmid  4679  ordsucunielexmid  4680  regexmidlem1  4682  elirr  4690  nordeq  4693  sucprcreg  4698  en2lp  4703  ordsoexmid  4711  ordsuc  4712  onsucuni2  4713  tfis  4732  peano2  4744  findes  4752  limom  4763  opelxp  4806  opeliunxp  4832  opbrop  4856  ssrel  4865  ssrel2  4867  ssrelrel  4877  relopabi  4907  eliunxp  4921  opeliunxp2  4922  ideqg  4933  reldmm  5002  dmmrnm  5003  dmxpm  5004  elreldm  5010  elrnmptg  5036  elres  5101  resiexg  5111  dfres2  5118  imai  5146  elimasng  5158  issref  5173  xpmlem  5211  xpm  5212  elxp4  5278  elxp5  5279  unielrel  5318  relcnvexb  5330  dmfex  5585  funfveu  5711  funimass4  5756  fvelimab  5762  ssimaex  5767  fvopab3g  5781  fvopab3ig  5782  fvmptssdm  5793  chfnrn  5823  fvelrn  5842  fmpt  5861  ffnfv  5869  fmptco  5877  elunirn  5975  f1elima  5982  cbvriota  6053  acexmidlemab  6082  acexmidlemcase  6083  cbvmpox  6169  eloprabga  6178  resoprab  6187  elrnmpo  6205  ov  6211  ovig  6213  ov6g  6230  ovg  6231  ovelrn  6241  caovimo  6286  abrexss  6362  fo1stresm  6399  fo2ndresm  6400  elxp6  6407  unielxp  6412  eqop2  6416  dfoprab4  6430  dfoprab4f  6431  fmpox  6440  1stconst  6461  2ndconst  6462  f1o2ndf1  6468  xporderlem  6471  f1od2  6475  disjxp1  6476  opeliunxp2f  6514  dftpos3  6538  dftpos4  6539  tpostpos  6540  smoel  6576  tfr1onlemaccex  6624  tfrcllemaccex  6637  tfrcl  6640  frecabcl  6675  frecsuc  6683  nntri3or  6771  nntri3  6775  nndcel  6778  riinerm  6887  th3qlem1  6916  mapsncnv  6983  elixpsn  7023  dom2lem  7064  fiprc  7110  xpsnen  7125  phplem3g  7163  phpelm  7174  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  elssdc  7215  inffiexmid  7219  undifdcss  7236  opabfi  7253  snon0  7255  f1dmvrnfibi  7264  f1vrnfibi  7265  relresfin  7270  isfsuppfid  7297  ordiso2  7381  ctssdclemn0  7456  ctssdc  7459  enumct  7461  nnnninf  7472  nnnninfeq  7474  nninfisollemne  7477  nninfisol  7479  finomni  7486  exmidlpo  7489  pr2cv1  7547  acneq  7564  finacn  7566  acfun  7569  exmidontriimlem3  7585  exmidontriimlem4  7586  pw1ne1  7594  onntri35  7602  exmidapne  7632  ccfunen  7636  cc2lem  7638  elni2  7687  recexnq  7763  recmulnqg  7764  enq0enq  7804  enq0sym  7805  enq0ref  7806  enq0tr  7807  enq0breq  7809  nqnq0pi  7811  nqnq0  7814  prop  7848  prcdnql  7857  prcunqu  7858  prubl  7859  prltlu  7860  prnmaxl  7861  prnminu  7862  prdisj  7865  prarloc  7876  genipv  7882  genpelvl  7885  genpelvu  7886  genprndl  7894  genprndu  7895  distrlem5prl  7959  distrlem5pru  7960  ltexprlemm  7973  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemm  8041  caucvgprlemladdfu  8050  caucvgprprlemmu  8068  elreal2  8203  ltresr  8212  axcnre  8254  axpre-suploclemres  8274  0re  8332  renepnf  8379  renemnf  8380  ltxrlt  8397  eqlei2  8427  0cnALT  8523  sup3exmid  9295  nn1suc  9332  nnne0  9341  xnn0xr  9644  nn0nepnf  9647  elz  9655  elnn0z  9666  elz2  9725  uzind4s  10005  elnn1uz2  10022  qre  10040  elpqb  10066  xnn0lenn0nn0  10283  xsubge0  10299  xposdif  10300  xleaddadd  10305  fzsn  10488  fz1sbc  10519  elfzp12  10522  fzm1  10523  fz01or  10534  fvinim0ffz  10676  suprzubdc  10687  zsupssdc  10689  xqltnle  10718  flqidz  10741  ceilqidz  10773  modqmuladdnn0  10825  frec2uzrand  10862  frecuzrdgtcl  10869  fzfig  10887  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  monoord  10942  seq3split  10945  seqsplitg  10946  iseqf1olemqval  10957  seq3id2  10983  seqhomog  10987  1exp  11025  bcval  11208  hashennn  11240  hashfibc  11304  zfz1isolem1  11313  zfz1iso  11314  seq3coll  11315  iswrdiz  11332  0wrd0  11351  lswlgt0cl  11378  ccatval1  11386  ccatval2  11387  ccatalpha  11402  ccatrcl1  11403  wrdl1s1  11419  ccats1val2  11429  wrd2ind  11516  pfxccatin12lem3  11525  pfxccatid  11534  reuccatpfxs1lem  11539  shftlem  11602  shftfibg  11606  shftfib  11609  shftfn  11610  2shfti  11617  rexuz3  11777  sqrt0rlem  11790  cau3  11903  negfi  12016  sumdc  12148  sumrbdclem  12168  summodclem2a  12172  fisumss  12183  prodrbdclem  12362  prodmodclem2a  12367  fprodssdc  12381  fprodsplit1f  12425  ef0lem  12451  odd2np1  12664  even2n  12665  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  nn0enne  12693  divalgmod  12718  uzwodc  12838  lcmgcdlem  12879  cncongr1  12905  1nprm  12916  isprm2  12919  dvdsnprmd  12927  prmdc  12932  exprmfct  12941  nprmdvds1  12943  coprm  12947  prmdiveq  13042  prm23lt5  13070  pcpre1  13099  pc2dvds  13137  pcz  13139  pcmpt  13150  qexpz  13159  4sqlem2  13196  4sqlem19  13216  prmlem0  13248  ballotfilem2  13285  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemhom  13363  ctiunctlemudc  13385  ssnnctlemct  13394  nninfdclemcl  13396  imasaddfnlemg  13693  ismgmid  13755  isgrpid2  13903  mhmlem  13975  eqgval  14084  dvdsrcl2  14514  nzrunit  14603  lringuplu  14611  dvdsrzring  15046  znrrg  15103  psrbagmax  15183  mplsubgfilemm  15231  fiinopn  15247  istopon  15256  basis2  15291  eltg3  15300  tg2  15303  tgidm  15317  bastop  15318  bastop2  15327  topnex  15329  isopn3  15368  tgrest  15412  cnpval  15441  lmbr  15456  cnconst  15477  txbas  15501  uptx  15517  txdis1cn  15521  cnmpt12  15530  cnmpt22  15537  hmeocnvb  15561  xblm  15660  isxms2  15695  mopni  15725  blssioo  15796  dedekindeulemuub  15860  dedekindeulemeu  15865  dedekindicclemuub  15869  dedekindicclemeu  15874  ivthinclemlm  15877  ivthinclemum  15878  ivthreinc  15888  pellexlem3  16248  bposlem5  16332  lgsfvalg  16346  lgsval2lem  16351  lgsdir2lem2  16370  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  gausslemma2dlem6  16408  2lgslem1b  16430  2lgs  16445  2lgsoddprmlem2  16447  2lgsoddprmlem3  16452  2sqlem2  16456  2sqlem6  16461  2sqlem7  16462  2sqlem10  16466  vtxvalg  16479  iedgvalg  16480  umgredg  16608  upgrpredgv  16609  usgredg2vlem2  16686  ushgredgedg  16689  ushgredgedgloop  16691  griedg0ssusgr  16714  uhgrspansubgrlem  16739  vtxdgfifival  16754  iswlk  16786  upgrwlkvtxedg  16827  isclwwlknx  16879  clwwlkn1loopb  16883  clwwlknonex2lem1  16900  elabgf0  17027  bj-rspgt  17036  cbvrald  17038  decidi  17045  sumdc2  17049  bdssex  17150  bj-inex  17155  bj-intnexr  17157  bj-unexg  17169  bj-d0clsepcl  17173  bj-nnelirr  17201  bj-nn0suc  17212  bj-inf2vnlem1  17218  bj-inf2vnlem2  17219  bj-inf2vnlem3  17220  bj-inf2vnlem4  17221  bj-nn0sucALT  17226  bj-findis  17227  3dom  17240  wexmiddiffilem  17265  wexmiddifxy  17268  trilpolemcl  17310