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  8480  sup3exmid  9251  nn1suc  9276  nnne0  9285  xnn0xr  9588  nn0nepnf  9591  elz  9599  elnn0z  9610  elz2  9669  uzind4s  9943  elnn1uz2  9960  qre  9978  elpqb  10003  xnn0lenn0nn0  10220  xsubge0  10236  xposdif  10237  xleaddadd  10242  fzsn  10424  fz1sbc  10455  elfzp12  10458  fzm1  10459  fz01or  10470  fvinim0ffz  10612  suprzubdc  10623  zsupssdc  10625  xqltnle  10654  flqidz  10673  ceilqidz  10705  modqmuladdnn0  10757  frec2uzrand  10794  frecuzrdgtcl  10801  fzfig  10819  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord  10874  seq3split  10877  seqsplitg  10878  iseqf1olemqval  10889  seq3id2  10915  seqhomog  10919  1exp  10957  bcval  11139  hashennn  11171  hashfibc  11235  zfz1isolem1  11240  zfz1iso  11241  seq3coll  11242  iswrdiz  11259  0wrd0  11278  lswlgt0cl  11305  ccatval1  11313  ccatval2  11314  ccatalpha  11329  ccatrcl1  11330  wrdl1s1  11346  ccats1val2  11356  wrd2ind  11443  pfxccatin12lem3  11452  pfxccatid  11461  reuccatpfxs1lem  11466  shftlem  11529  shftfibg  11533  shftfib  11536  shftfn  11537  2shfti  11544  rexuz3  11703  sqrt0rlem  11716  cau3  11828  negfi  11941  sumdc  12071  sumrbdclem  12091  summodclem2a  12095  fisumss  12106  prodrbdclem  12285  prodmodclem2a  12290  fprodssdc  12304  fprodsplit1f  12348  ef0lem  12374  odd2np1  12587  even2n  12588  oddnn02np1  12594  oddge22np1  12595  evennn02n  12596  evennn2n  12597  nn0enne  12616  divalgmod  12641  uzwodc  12761  lcmgcdlem  12802  cncongr1  12828  1nprm  12839  isprm2  12842  dvdsnprmd  12850  prmdc  12855  exprmfct  12863  nprmdvds1  12865  coprm  12869  prmdiveq  12961  prm23lt5  12989  pcpre1  13018  pc2dvds  13056  pcz  13058  pcmpt  13069  qexpz  13078  4sqlem2  13115  4sqlem19  13135  ballotfilem2  13175  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemhom  13253  ctiunctlemudc  13275  ssnnctlemct  13284  nninfdclemcl  13286  imasaddfnlemg  13581  ismgmid  13643  isgrpid2  13798  mhmlem  13870  eqgval  13979  dvdsrcl2  14347  nzrunit  14436  lringuplu  14444  dvdsrzring  14880  znrrg  14937  mplsubgfilemm  14982  fiinopn  14998  istopon  15007  basis2  15042  eltg3  15051  tg2  15054  tgidm  15068  bastop  15069  bastop2  15078  topnex  15080  isopn3  15119  tgrest  15163  cnpval  15192  lmbr  15207  cnconst  15228  txbas  15252  uptx  15268  txdis1cn  15272  cnmpt12  15281  cnmpt22  15288  hmeocnvb  15312  xblm  15411  isxms2  15446  mopni  15476  blssioo  15547  dedekindeulemuub  15611  dedekindeulemeu  15616  dedekindicclemuub  15620  dedekindicclemeu  15625  ivthinclemlm  15628  ivthinclemum  15629  ivthreinc  15639  pellexlem3  15976  lgsfvalg  16007  lgsval2lem  16012  lgsdir2lem2  16031  gausslemma2dlem1a  16060  gausslemma2dlem4  16066  gausslemma2dlem6  16069  2lgslem1b  16091  2lgs  16106  2lgsoddprmlem2  16108  2lgsoddprmlem3  16113  2sqlem2  16117  2sqlem6  16122  2sqlem7  16123  2sqlem10  16127  vtxvalg  16140  iedgvalg  16141  umgredg  16269  upgrpredgv  16270  usgredg2vlem2  16347  ushgredgedg  16350  ushgredgedgloop  16352  griedg0ssusgr  16375  uhgrspansubgrlem  16400  vtxdgfifival  16415  iswlk  16447  upgrwlkvtxedg  16488  isclwwlknx  16540  clwwlkn1loopb  16544  clwwlknonex2lem1  16561  elabgf0  16688  bj-rspgt  16697  cbvrald  16699  decidi  16706  sumdc2  16710  bdssex  16811  bj-inex  16816  bj-intnexr  16818  bj-unexg  16830  bj-d0clsepcl  16834  bj-nnelirr  16862  bj-nn0suc  16873  bj-inf2vnlem1  16879  bj-inf2vnlem2  16880  bj-inf2vnlem3  16881  bj-inf2vnlem4  16882  bj-nn0sucALT  16887  bj-findis  16888  3dom  16901  trilpolemcl  16960