Theorem eleq1 2292

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395  ∃wex 1538   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  eleq12  2294  eleq1i  2295  eleq1d  2298  eleq1a  2301  cleqh  2329  nelneq  2330  clelsb1  2334  nfcjust  2360  cleqf  2397  nelne2  2491  neleq1  2499  rgen2a  2584  cbvralf  2756  cbvrexf  2757  cbvreu  2763  cbvrab  2797  eqvisset  2810  ceqsralt  2827  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  rspce  2902  rspc2gv  2919  ceqsrexv  2933  ceqsrexbv  2934  clel2  2936  elabgt  2944  elabgf  2945  elrabi  2956  elrabf  2957  elrab3t  2958  ralab2  2967  rexab2  2969  mo2icl  2982  morex  2987  reu2  2991  reu6  2992  rmo4  2996  reu8  2999  reuind  3008  nelrdva  3010  ru  3027  dfsbcq  3030  dfsbcq2  3031  sbc8g  3036  sbcel1v  3091  rmob  3122  difjust  3198  unjust  3200  injust  3202  eldif  3206  dfss2f  3215  uniiunlem  3313  elun  3345  elin  3387  rabn0m  3519  disjne  3545  r19.3rm  3580  r19.9rmv  3583  raaanlem  3596  raaan  3597  elif  3614  ifmdc  3645  elpwg  3657  elpr2  3688  elsn2g  3699  rabsn  3733  tpid3g  3781  snssb  3800  snssgOLD  3803  difsn  3804  sssnm  3831  opeq1  3856  opeq2  3857  eluni  3890  elunii  3892  eluniab  3899  elint  3928  elintg  3930  elintab  3933  elintrabg  3935  intss1  3937  eliun  3968  eliin  3969  dfiunv2  4000  opabss  4147  cbvmpt  4178  trel  4188  trss  4190  ssex  4220  intnexr  4234  intexabim  4235  exmidel  4288  euabex  4310  elopab  4345  opelopab2a  4352  frirrg  4440  tz7.2  4444  ordelord  4471  onm  4491  ralxfr2d  4554  rexxfr2d  4555  rabxfrd  4559  reuhypd  4561  ordtriexmid  4612  ontriexmidim  4613  ordtri2orexmid  4614  ontr2exmid  4616  onsucsssucexmid  4618  onsucelsucexmid  4621  ordsucunielexmid  4622  regexmidlem1  4624  elirr  4632  nordeq  4635  sucprcreg  4640  en2lp  4645  ordsoexmid  4653  ordsuc  4654  onsucuni2  4655  tfis  4674  peano2  4686  findes  4694  limom  4705  opelxp  4748  opeliunxp  4773  opbrop  4797  ssrel  4806  ssrel2  4808  ssrelrel  4818  relopabi  4846  eliunxp  4860  opeliunxp2  4861  ideqg  4872  reldmm  4941  dmmrnm  4942  dmxpm  4943  elreldm  4949  elrnmptg  4975  elres  5040  resiexg  5049  dfres2  5056  imai  5083  elimasng  5095  issref  5110  xpmlem  5148  xpm  5149  elxp4  5215  elxp5  5216  unielrel  5255  relcnvexb  5267  dmfex  5514  funfveu  5639  funimass4  5683  fvelimab  5689  ssimaex  5694  fvopab3g  5706  fvopab3ig  5707  fvmptssdm  5718  chfnrn  5745  fvelrn  5765  fmpt  5784  ffnfv  5792  fmptco  5800  elunirn  5889  f1elima  5896  cbvriota  5965  acexmidlemab  5994  acexmidlemcase  5995  cbvmpox  6081  eloprabga  6090  resoprab  6099  elrnmpo  6117  ov  6123  ovig  6125  ov6g  6142  ovg  6143  ovelrn  6153  caovimo  6198  fo1stresm  6305  fo2ndresm  6306  elxp6  6313  unielxp  6318  eqop2  6322  dfoprab4  6336  dfoprab4f  6337  fmpox  6344  1stconst  6365  2ndconst  6366  f1o2ndf1  6372  xporderlem  6375  f1od2  6379  disjxp1  6380  opeliunxp2f  6382  dftpos3  6406  dftpos4  6407  tpostpos  6408  smoel  6444  tfr1onlemaccex  6492  tfrcllemaccex  6505  tfrcl  6508  frecabcl  6543  frecsuc  6551  nntri3or  6637  nntri3  6641  nndcel  6644  riinerm  6753  th3qlem1  6782  mapsncnv  6840  elixpsn  6880  dom2lem  6921  fiprc  6966  xpsnen  6976  phplem3g  7013  phpelm  7024  ssfiexmid  7034  domfiexmid  7036  inffiexmid  7064  undifdcss  7081  opabfi  7096  snon0  7098  f1dmvrnfibi  7107  f1vrnfibi  7108  ordiso2  7198  ctssdclemn0  7273  ctssdc  7276  enumct  7278  nnnninf  7289  nnnninfeq  7291  nninfisollemne  7294  nninfisol  7296  finomni  7303  exmidlpo  7306  pr2cv1  7364  acneq  7380  finacn  7382  acfun  7385  exmidontriimlem3  7401  exmidontriimlem4  7402  pw1ne1  7410  onntri35  7418  exmidapne  7442  ccfunen  7446  cc2lem  7448  elni2  7497  recexnq  7573  recmulnqg  7574  enq0enq  7614  enq0sym  7615  enq0ref  7616  enq0tr  7617  enq0breq  7619  nqnq0pi  7621  nqnq0  7624  prop  7658  prcdnql  7667  prcunqu  7668  prubl  7669  prltlu  7670  prnmaxl  7671  prnminu  7672  prdisj  7675  prarloc  7686  genipv  7692  genpelvl  7695  genpelvu  7696  genprndl  7704  genprndu  7705  distrlem5prl  7769  distrlem5pru  7770  ltexprlemm  7783  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemrl  7793  ltexprlemru  7795  aptiprleml  7822  aptiprlemu  7823  archpr  7826  cauappcvgprlemm  7828  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  caucvgprlemm  7851  caucvgprlemladdfu  7860  caucvgprprlemmu  7878  elreal2  8013  ltresr  8022  axcnre  8064  axpre-suploclemres  8084  0re  8142  renepnf  8190  renemnf  8191  ltxrlt  8208  eqlei2  8237  0cnALT  8332  sup3exmid  9100  nn1suc  9125  nnne0  9134  xnn0xr  9433  nn0nepnf  9436  elz  9444  elnn0z  9455  elz2  9514  uzind4s  9781  elnn1uz2  9798  qre  9816  elpqb  9841  xnn0lenn0nn0  10057  xsubge0  10073  xposdif  10074  xleaddadd  10079  fzsn  10258  fz1sbc  10288  elfzp12  10291  fzm1  10292  fz01or  10303  fvinim0ffz  10442  suprzubdc  10451  zsupssdc  10453  xqltnle  10482  flqidz  10501  ceilqidz  10533  modqmuladdnn0  10585  frec2uzrand  10622  frecuzrdgtcl  10629  fzfig  10647  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord  10702  seq3split  10705  seqsplitg  10706  iseqf1olemqval  10717  seq3id2  10743  seqhomog  10747  1exp  10785  bcval  10966  hashennn  10997  zfz1isolem1  11057  zfz1iso  11058  seq3coll  11059  iswrdiz  11073  0wrd0  11092  lswlgt0cl  11119  ccatval1  11127  ccatval2  11128  wrdl1s1  11158  ccats1val2  11166  wrd2ind  11250  pfxccatin12lem3  11259  pfxccatid  11268  reuccatpfxs1lem  11273  shftlem  11322  shftfibg  11326  shftfib  11329  shftfn  11330  2shfti  11337  rexuz3  11496  sqrt0rlem  11509  cau3  11621  negfi  11734  sumdc  11864  sumrbdclem  11883  summodclem2a  11887  fisumss  11898  prodrbdclem  12077  prodmodclem2a  12082  fprodssdc  12096  fprodsplit1f  12140  ef0lem  12166  odd2np1  12379  even2n  12380  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  nn0enne  12408  divalgmod  12433  uzwodc  12553  lcmgcdlem  12594  cncongr1  12620  1nprm  12631  isprm2  12634  dvdsnprmd  12642  prmdc  12647  exprmfct  12655  nprmdvds1  12657  coprm  12661  prmdiveq  12753  prm23lt5  12781  pcpre1  12810  pc2dvds  12848  pcz  12850  pcmpt  12861  qexpz  12870  4sqlem2  12907  4sqlem19  12927  ennnfonelemhom  12981  ctiunctlemudc  13003  ssnnctlemct  13012  nninfdclemcl  13014  imasaddfnlemg  13342  ismgmid  13405  isgrpid2  13568  mhmlem  13646  eqgval  13755  dvdsrcl2  14057  nzrunit  14146  lringuplu  14154  dvdsrzring  14561  znrrg  14618  mplsubgfilemm  14656  fiinopn  14672  istopon  14681  basis2  14716  eltg3  14725  tg2  14728  tgidm  14742  bastop  14743  bastop2  14752  topnex  14754  isopn3  14793  tgrest  14837  cnpval  14866  lmbr  14881  cnconst  14902  txbas  14926  uptx  14942  txdis1cn  14946  cnmpt12  14955  cnmpt22  14962  hmeocnvb  14986  xblm  15085  isxms2  15120  mopni  15150  blssioo  15221  dedekindeulemuub  15285  dedekindeulemeu  15290  dedekindicclemuub  15294  dedekindicclemeu  15299  ivthinclemlm  15302  ivthinclemum  15303  ivthreinc  15313  lgsfvalg  15678  lgsval2lem  15683  lgsdir2lem2  15702  gausslemma2dlem1a  15731  gausslemma2dlem4  15737  gausslemma2dlem6  15740  2lgslem1b  15762  2lgs  15777  2lgsoddprmlem2  15779  2lgsoddprmlem3  15784  2sqlem2  15788  2sqlem6  15793  2sqlem7  15794  2sqlem10  15798  vtxvalg  15811  iedgvalg  15812  umgredg  15937  upgrpredgv  15938  usgredg2vlem2  16015  ushgredgedg  16018  ushgredgedgloop  16020  iswlk  16029  elabgf0  16099  bj-rspgt  16108  cbvrald  16110  decidi  16117  sumdc2  16121  bdssex  16223  bj-inex  16228  bj-intnexr  16230  bj-unexg  16242  bj-d0clsepcl  16246  bj-nnelirr  16274  bj-nn0suc  16285  bj-inf2vnlem1  16291  bj-inf2vnlem2  16292  bj-inf2vnlem3  16293  bj-inf2vnlem4  16294  bj-nn0sucALT  16299  bj-findis  16300  trilpolemcl  16364