Theorem eleq1 2297

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398  ∃wex 1541   ∈ wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  eleq12  2299  eleq1i  2300  eleq1d  2303  eleq1a  2306  cleqh  2334  nelneq  2335  clelsb1  2339  nfcjust  2374  cleqf  2411  nelne2  2505  neleq1  2513  rgen2a  2598  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvrab  2813  eqvisset  2826  ceqsralt  2843  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  rspct  2916  rspc  2917  rspce  2918  rspc2gv  2936  ceqsrexv  2950  ceqsrexbv  2951  clel2  2953  elabgt  2961  elabgf  2962  elrabi  2973  elrabf  2974  elrab3t  2975  ralab2  2984  rexab2  2986  mo2icl  2999  morex  3004  reu2  3008  reu6  3009  rmo4  3013  reu8  3016  reuind  3025  nelrdva  3027  ru  3044  dfsbcq  3047  dfsbcq2  3048  sbc8g  3053  sbcel1v  3108  rmob  3139  difjust  3215  unjust  3217  injust  3219  eldif  3223  dfssf  3232  dfss2f  3233  uniiunlem  3332  elun  3364  elin  3406  rabn0m  3540  disjne  3566  r19.3rm  3602  r19.9rmv  3605  raaanlem  3618  raaan  3619  elif  3638  ifmdc  3669  elpwg  3682  elpr2  3716  elsn2g  3727  rabsn  3761  tpid3g  3812  snssb  3832  snssgOLD  3835  difsn  3836  sssnm  3863  opeq1  3888  opeq2  3889  eluni  3922  elunii  3924  eluniab  3931  elint  3960  elintg  3962  elintab  3965  elintrabg  3967  intss1  3969  eliun  4000  eliin  4001  dfiunv2  4032  opabss  4179  cbvmpt  4210  trel  4220  trss  4222  ssex  4252  intnexr  4268  intexabim  4269  exmidel  4323  euabex  4346  elopab  4381  opelopab2a  4388  frirrg  4476  tz7.2  4480  ordelord  4507  onm  4527  ralxfr2d  4590  rexxfr2d  4591  rabxfrd  4595  reuhypd  4597  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmid  4657  ordsucunielexmid  4658  regexmidlem1  4660  elirr  4668  nordeq  4671  sucprcreg  4676  en2lp  4681  ordsoexmid  4689  ordsuc  4690  onsucuni2  4691  tfis  4710  peano2  4722  findes  4730  limom  4741  opelxp  4784  opeliunxp  4810  opbrop  4834  ssrel  4843  ssrel2  4845  ssrelrel  4855  relopabi  4885  eliunxp  4899  opeliunxp2  4900  ideqg  4911  reldmm  4980  dmmrnm  4981  dmxpm  4982  elreldm  4988  elrnmptg  5014  elres  5079  resiexg  5088  dfres2  5095  imai  5123  elimasng  5135  issref  5150  xpmlem  5188  xpm  5189  elxp4  5255  elxp5  5256  unielrel  5295  relcnvexb  5307  dmfex  5562  funfveu  5688  funimass4  5732  fvelimab  5738  ssimaex  5743  fvopab3g  5755  fvopab3ig  5756  fvmptssdm  5767  chfnrn  5794  fvelrn  5813  fmpt  5832  ffnfv  5840  fmptco  5848  elunirn  5945  f1elima  5952  cbvriota  6023  acexmidlemab  6052  acexmidlemcase  6053  cbvmpox  6139  eloprabga  6148  resoprab  6157  elrnmpo  6175  ov  6181  ovig  6183  ov6g  6200  ovg  6201  ovelrn  6211  caovimo  6256  abrexss  6331  fo1stresm  6368  fo2ndresm  6369  elxp6  6376  unielxp  6381  eqop2  6385  dfoprab4  6399  dfoprab4f  6400  fmpox  6409  1stconst  6430  2ndconst  6431  f1o2ndf1  6437  xporderlem  6440  f1od2  6444  disjxp1  6445  opeliunxp2f  6482  dftpos3  6506  dftpos4  6507  tpostpos  6508  smoel  6544  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcl  6608  frecabcl  6643  frecsuc  6651  nntri3or  6739  nntri3  6743  nndcel  6746  riinerm  6855  th3qlem1  6884  mapsncnv  6943  elixpsn  6983  dom2lem  7024  fiprc  7070  xpsnen  7085  phplem3g  7123  phpelm  7134  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  elssdc  7175  inffiexmid  7179  undifdcss  7196  opabfi  7213  snon0  7215  f1dmvrnfibi  7224  f1vrnfibi  7225  suppeqfsuppbi  7261  ordiso2  7339  ctssdclemn0  7414  ctssdc  7417  enumct  7419  nnnninf  7430  nnnninfeq  7432  nninfisollemne  7435  nninfisol  7437  finomni  7444  exmidlpo  7447  pr2cv1  7505  acneq  7522  finacn  7524  acfun  7527  exmidontriimlem3  7543  exmidontriimlem4  7544  pw1ne1  7552  onntri35  7560  exmidapne  7590  ccfunen  7594  cc2lem  7596  elni2  7645  recexnq  7721  recmulnqg  7722  enq0enq  7762  enq0sym  7763  enq0ref  7764  enq0tr  7765  enq0breq  7767  nqnq0pi  7769  nqnq0  7772  prop  7806  prcdnql  7815  prcunqu  7816  prubl  7817  prltlu  7818  prnmaxl  7819  prnminu  7820  prdisj  7823  prarloc  7834  genipv  7840  genpelvl  7843  genpelvu  7844  genprndl  7852  genprndu  7853  distrlem5prl  7917  distrlem5pru  7918  ltexprlemm  7931  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  aptiprleml  7970  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  caucvgprlemm  7999  caucvgprlemladdfu  8008  caucvgprprlemmu  8026  elreal2  8161  ltresr  8170  axcnre  8212  axpre-suploclemres  8232  0re  8290  renepnf  8337  renemnf  8338  ltxrlt  8355  eqlei2  8384  0cnALT  8479  sup3exmid  9248  nn1suc  9273  nnne0  9282  xnn0xr  9585  nn0nepnf  9588  elz  9596  elnn0z  9607  elz2  9666  uzind4s  9940  elnn1uz2  9957  qre  9975  elpqb  10000  xnn0lenn0nn0  10217  xsubge0  10233  xposdif  10234  xleaddadd  10239  fzsn  10421  fz1sbc  10452  elfzp12  10455  fzm1  10456  fz01or  10467  fvinim0ffz  10609  suprzubdc  10620  zsupssdc  10622  xqltnle  10651  flqidz  10670  ceilqidz  10702  modqmuladdnn0  10754  frec2uzrand  10791  frecuzrdgtcl  10798  fzfig  10816  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  monoord  10871  seq3split  10874  seqsplitg  10875  iseqf1olemqval  10886  seq3id2  10912  seqhomog  10916  1exp  10954  bcval  11136  hashennn  11168  hashfibc  11232  zfz1isolem1  11237  zfz1iso  11238  seq3coll  11239  iswrdiz  11256  0wrd0  11275  lswlgt0cl  11302  ccatval1  11310  ccatval2  11311  ccatalpha  11326  ccatrcl1  11327  wrdl1s1  11343  ccats1val2  11353  wrd2ind  11440  pfxccatin12lem3  11449  pfxccatid  11458  reuccatpfxs1lem  11463  shftlem  11526  shftfibg  11530  shftfib  11533  shftfn  11534  2shfti  11541  rexuz3  11700  sqrt0rlem  11713  cau3  11825  negfi  11938  sumdc  12068  sumrbdclem  12088  summodclem2a  12092  fisumss  12103  prodrbdclem  12282  prodmodclem2a  12287  fprodssdc  12301  fprodsplit1f  12345  ef0lem  12371  odd2np1  12584  even2n  12585  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  nn0enne  12613  divalgmod  12638  uzwodc  12758  lcmgcdlem  12799  cncongr1  12825  1nprm  12836  isprm2  12839  dvdsnprmd  12847  prmdc  12852  exprmfct  12860  nprmdvds1  12862  coprm  12866  prmdiveq  12958  prm23lt5  12986  pcpre1  13015  pc2dvds  13053  pcz  13055  pcmpt  13066  qexpz  13075  4sqlem2  13112  4sqlem19  13132  ballotfilem2  13172  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemhom  13250  ctiunctlemudc  13272  ssnnctlemct  13281  nninfdclemcl  13283  imasaddfnlemg  13578  ismgmid  13640  isgrpid2  13795  mhmlem  13867  eqgval  13976  dvdsrcl2  14344  nzrunit  14433  lringuplu  14441  dvdsrzring  14877  znrrg  14934  mplsubgfilemm  14979  fiinopn  14995  istopon  15004  basis2  15039  eltg3  15048  tg2  15051  tgidm  15065  bastop  15066  bastop2  15075  topnex  15077  isopn3  15116  tgrest  15160  cnpval  15189  lmbr  15204  cnconst  15225  txbas  15249  uptx  15265  txdis1cn  15269  cnmpt12  15278  cnmpt22  15285  hmeocnvb  15309  xblm  15408  isxms2  15443  mopni  15473  blssioo  15544  dedekindeulemuub  15608  dedekindeulemeu  15613  dedekindicclemuub  15617  dedekindicclemeu  15622  ivthinclemlm  15625  ivthinclemum  15626  ivthreinc  15636  pellexlem3  15973  lgsfvalg  16004  lgsval2lem  16009  lgsdir2lem2  16028  gausslemma2dlem1a  16057  gausslemma2dlem4  16063  gausslemma2dlem6  16066  2lgslem1b  16088  2lgs  16103  2lgsoddprmlem2  16105  2lgsoddprmlem3  16110  2sqlem2  16114  2sqlem6  16119  2sqlem7  16120  2sqlem10  16124  vtxvalg  16137  iedgvalg  16138  umgredg  16266  upgrpredgv  16267  usgredg2vlem2  16344  ushgredgedg  16347  ushgredgedgloop  16349  griedg0ssusgr  16372  uhgrspansubgrlem  16397  vtxdgfifival  16412  iswlk  16444  upgrwlkvtxedg  16485  isclwwlknx  16537  clwwlkn1loopb  16541  clwwlknonex2lem1  16558  elabgf0  16675  bj-rspgt  16684  cbvrald  16686  decidi  16693  sumdc2  16697  bdssex  16798  bj-inex  16803  bj-intnexr  16805  bj-unexg  16817  bj-d0clsepcl  16821  bj-nnelirr  16849  bj-nn0suc  16860  bj-inf2vnlem1  16866  bj-inf2vnlem2  16867  bj-inf2vnlem3  16868  bj-inf2vnlem4  16869  bj-nn0sucALT  16874  bj-findis  16875  3dom  16888  trilpolemcl  16947