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 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced 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  3577  r19.3rm  3613  r19.9rmv  3616  raaanlem  3629  raaan  3630  elif  3649  ifmdc  3680  elpwg  3693  elpr2  3727  elsn2g  3738  rabsn  3772  tpid3g  3823  snssb  3843  snssgOLD  3846  difsn  3847  sssnm  3874  opeq1  3899  opeq2  3900  eluni  3933  elunii  3935  eluniab  3942  elint  3971  elintg  3973  elintab  3976  elintrabg  3978  intss1  3980  eliun  4011  eliin  4012  dfiunv2  4043  opabss  4190  cbvmpt  4221  trel  4231  trss  4233  ssex  4265  intnexr  4282  intexabim  4283  exmidel  4337  euabex  4360  elopab  4395  opelopab2a  4402  frirrg  4490  tz7.2  4494  ordelord  4521  onm  4541  ralxfr2d  4605  rexxfr2d  4606  rabxfrd  4610  reuhypd  4612  ordtriexmid  4663  ontriexmidim  4664  ordtri2orexmid  4665  ontr2exmid  4667  onsucsssucexmid  4669  onsucelsucexmid  4672  ordsucunielexmid  4673  regexmidlem1  4675  elirr  4683  nordeq  4686  sucprcreg  4691  en2lp  4696  ordsoexmid  4704  ordsuc  4705  onsucuni2  4706  tfis  4725  peano2  4737  findes  4745  limom  4756  opelxp  4799  opeliunxp  4825  opbrop  4849  ssrel  4858  ssrel2  4860  ssrelrel  4870  relopabi  4900  eliunxp  4914  opeliunxp2  4915  ideqg  4926  reldmm  4995  dmmrnm  4996  dmxpm  4997  elreldm  5003  elrnmptg  5029  elres  5094  resiexg  5103  dfres2  5110  imai  5138  elimasng  5150  issref  5165  xpmlem  5203  xpm  5204  elxp4  5270  elxp5  5271  unielrel  5310  relcnvexb  5322  dmfex  5577  funfveu  5703  funimass4  5747  fvelimab  5753  ssimaex  5758  fvopab3g  5772  fvopab3ig  5773  fvmptssdm  5784  chfnrn  5811  fvelrn  5830  fmpt  5849  ffnfv  5857  fmptco  5865  elunirn  5962  f1elima  5969  cbvriota  6040  acexmidlemab  6069  acexmidlemcase  6070  cbvmpox  6156  eloprabga  6165  resoprab  6174  elrnmpo  6192  ov  6198  ovig  6200  ov6g  6217  ovg  6218  ovelrn  6228  caovimo  6273  abrexss  6348  fo1stresm  6385  fo2ndresm  6386  elxp6  6393  unielxp  6398  eqop2  6402  dfoprab4  6416  dfoprab4f  6417  fmpox  6426  1stconst  6447  2ndconst  6448  f1o2ndf1  6454  xporderlem  6457  f1od2  6461  disjxp1  6462  opeliunxp2f  6499  dftpos3  6523  dftpos4  6524  tpostpos  6525  smoel  6561  tfr1onlemaccex  6609  tfrcllemaccex  6622  tfrcl  6625  frecabcl  6660  frecsuc  6668  nntri3or  6756  nntri3  6760  nndcel  6763  riinerm  6872  th3qlem1  6901  mapsncnv  6967  elixpsn  7007  dom2lem  7048  fiprc  7094  xpsnen  7109  phplem3g  7147  phpelm  7158  ssfiexmid  7168  ssfiexmidt  7170  domfiexmid  7172  elssdc  7199  inffiexmid  7203  undifdcss  7220  opabfi  7237  snon0  7239  f1dmvrnfibi  7248  f1vrnfibi  7249  suppeqfsuppbi  7285  ordiso2  7365  ctssdclemn0  7440  ctssdc  7443  enumct  7445  nnnninf  7456  nnnninfeq  7458  nninfisollemne  7461  nninfisol  7463  finomni  7470  exmidlpo  7473  pr2cv1  7531  acneq  7548  finacn  7550  acfun  7553  exmidontriimlem3  7569  exmidontriimlem4  7570  pw1ne1  7578  onntri35  7586  exmidapne  7616  ccfunen  7620  cc2lem  7622  elni2  7671  recexnq  7747  recmulnqg  7748  enq0enq  7788  enq0sym  7789  enq0ref  7790  enq0tr  7791  enq0breq  7793  nqnq0pi  7795  nqnq0  7798  prop  7832  prcdnql  7841  prcunqu  7842  prubl  7843  prltlu  7844  prnmaxl  7845  prnminu  7846  prdisj  7849  prarloc  7860  genipv  7866  genpelvl  7869  genpelvu  7870  genprndl  7878  genprndu  7879  distrlem5prl  7943  distrlem5pru  7944  ltexprlemm  7957  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  aptiprleml  7996  aptiprlemu  7997  archpr  8000  cauappcvgprlemm  8002  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  caucvgprlemm  8025  caucvgprlemladdfu  8034  caucvgprprlemmu  8052  elreal2  8187  ltresr  8196  axcnre  8238  axpre-suploclemres  8258  0re  8316  renepnf  8363  renemnf  8364  ltxrlt  8381  eqlei2  8410  0cnALT  8506  sup3exmid  9277  nn1suc  9302  nnne0  9311  xnn0xr  9614  nn0nepnf  9617  elz  9625  elnn0z  9636  elz2  9695  uzind4s  9969  elnn1uz2  9986  qre  10004  elpqb  10029  xnn0lenn0nn0  10246  xsubge0  10262  xposdif  10263  xleaddadd  10268  fzsn  10450  fz1sbc  10481  elfzp12  10484  fzm1  10485  fz01or  10496  fvinim0ffz  10638  suprzubdc  10649  zsupssdc  10651  xqltnle  10680  flqidz  10699  ceilqidz  10731  modqmuladdnn0  10783  frec2uzrand  10820  frecuzrdgtcl  10827  fzfig  10845  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  monoord  10900  seq3split  10903  seqsplitg  10904  iseqf1olemqval  10915  seq3id2  10941  seqhomog  10945  1exp  10983  bcval  11165  hashennn  11197  hashfibc  11261  zfz1isolem1  11270  zfz1iso  11271  seq3coll  11272  iswrdiz  11289  0wrd0  11308  lswlgt0cl  11335  ccatval1  11343  ccatval2  11344  ccatalpha  11359  ccatrcl1  11360  wrdl1s1  11376  ccats1val2  11386  wrd2ind  11473  pfxccatin12lem3  11482  pfxccatid  11491  reuccatpfxs1lem  11496  shftlem  11559  shftfibg  11563  shftfib  11566  shftfn  11567  2shfti  11574  rexuz3  11734  sqrt0rlem  11747  cau3  11859  negfi  11972  sumdc  12102  sumrbdclem  12122  summodclem2a  12126  fisumss  12137  prodrbdclem  12316  prodmodclem2a  12321  fprodssdc  12335  fprodsplit1f  12379  ef0lem  12405  odd2np1  12618  even2n  12619  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  nn0enne  12647  divalgmod  12672  uzwodc  12792  lcmgcdlem  12833  cncongr1  12859  1nprm  12870  isprm2  12873  dvdsnprmd  12881  prmdc  12886  exprmfct  12894  nprmdvds1  12896  coprm  12900  prmdiveq  12992  prm23lt5  13020  pcpre1  13049  pc2dvds  13087  pcz  13089  pcmpt  13100  qexpz  13109  4sqlem2  13146  4sqlem19  13166  ballotfilem2  13206  ballotfilemfc0  13210  ballotfilemfcc  13211  ennnfonelemhom  13284  ctiunctlemudc  13306  ssnnctlemct  13315  nninfdclemcl  13317  imasaddfnlemg  13612  ismgmid  13674  isgrpid2  13822  mhmlem  13894  eqgval  14003  dvdsrcl2  14379  nzrunit  14468  lringuplu  14476  dvdsrzring  14910  znrrg  14967  mplsubgfilemm  15012  fiinopn  15028  istopon  15037  basis2  15072  eltg3  15081  tg2  15084  tgidm  15098  bastop  15099  bastop2  15108  topnex  15110  isopn3  15149  tgrest  15193  cnpval  15222  lmbr  15237  cnconst  15258  txbas  15282  uptx  15298  txdis1cn  15302  cnmpt12  15311  cnmpt22  15318  hmeocnvb  15342  xblm  15441  isxms2  15476  mopni  15506  blssioo  15577  dedekindeulemuub  15641  dedekindeulemeu  15646  dedekindicclemuub  15650  dedekindicclemeu  15655  ivthinclemlm  15658  ivthinclemum  15659  ivthreinc  15669  pellexlem3  16007  lgsfvalg  16038  lgsval2lem  16043  lgsdir2lem2  16062  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  gausslemma2dlem6  16100  2lgslem1b  16122  2lgs  16137  2lgsoddprmlem2  16139  2lgsoddprmlem3  16144  2sqlem2  16148  2sqlem6  16153  2sqlem7  16154  2sqlem10  16158  vtxvalg  16171  iedgvalg  16172  umgredg  16300  upgrpredgv  16301  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  griedg0ssusgr  16406  uhgrspansubgrlem  16431  vtxdgfifival  16446  iswlk  16478  upgrwlkvtxedg  16519  isclwwlknx  16571  clwwlkn1loopb  16575  clwwlknonex2lem1  16592  elabgf0  16719  bj-rspgt  16728  cbvrald  16730  decidi  16737  sumdc2  16741  bdssex  16842  bj-inex  16847  bj-intnexr  16849  bj-unexg  16861  bj-d0clsepcl  16865  bj-nnelirr  16893  bj-nn0suc  16904  bj-inf2vnlem1  16910  bj-inf2vnlem2  16911  bj-inf2vnlem3  16912  bj-inf2vnlem4  16913  bj-nn0sucALT  16918  bj-findis  16919  3dom  16932  trilpolemcl  16991