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  4195  cbvmpt  4226  trel  4236  trss  4238  ssex  4270  intnexr  4287  intexabim  4288  exmidel  4342  euabex  4365  elopab  4400  opelopab2a  4407  frirrg  4495  tz7.2  4499  ordelord  4526  onm  4546  ralxfr2d  4610  rexxfr2d  4611  rabxfrd  4615  reuhypd  4617  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  ordsucunielexmid  4678  regexmidlem1  4680  elirr  4688  nordeq  4691  sucprcreg  4696  en2lp  4701  ordsoexmid  4709  ordsuc  4710  onsucuni2  4711  tfis  4730  peano2  4742  findes  4750  limom  4761  opelxp  4804  opeliunxp  4830  opbrop  4854  ssrel  4863  ssrel2  4865  ssrelrel  4875  relopabi  4905  eliunxp  4919  opeliunxp2  4920  ideqg  4931  reldmm  5000  dmmrnm  5001  dmxpm  5002  elreldm  5008  elrnmptg  5034  elres  5099  resiexg  5108  dfres2  5115  imai  5143  elimasng  5155  issref  5170  xpmlem  5208  xpm  5209  elxp4  5275  elxp5  5276  unielrel  5315  relcnvexb  5327  dmfex  5582  funfveu  5708  funimass4  5753  fvelimab  5759  ssimaex  5764  fvopab3g  5778  fvopab3ig  5779  fvmptssdm  5790  chfnrn  5820  fvelrn  5839  fmpt  5858  ffnfv  5866  fmptco  5874  elunirn  5972  f1elima  5979  cbvriota  6050  acexmidlemab  6079  acexmidlemcase  6080  cbvmpox  6166  eloprabga  6175  resoprab  6184  elrnmpo  6202  ov  6208  ovig  6210  ov6g  6227  ovg  6228  ovelrn  6238  caovimo  6283  abrexss  6358  fo1stresm  6395  fo2ndresm  6396  elxp6  6403  unielxp  6408  eqop2  6412  dfoprab4  6426  dfoprab4f  6427  fmpox  6436  1stconst  6457  2ndconst  6458  f1o2ndf1  6464  xporderlem  6467  f1od2  6471  disjxp1  6472  opeliunxp2f  6509  dftpos3  6533  dftpos4  6534  tpostpos  6535  smoel  6571  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  frecabcl  6670  frecsuc  6678  nntri3or  6766  nntri3  6770  nndcel  6773  riinerm  6882  th3qlem1  6911  mapsncnv  6977  elixpsn  7017  dom2lem  7058  fiprc  7104  xpsnen  7119  phplem3g  7157  phpelm  7168  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  elssdc  7209  inffiexmid  7213  undifdcss  7230  opabfi  7247  snon0  7249  f1dmvrnfibi  7258  f1vrnfibi  7259  suppeqfsuppbi  7295  ordiso2  7375  ctssdclemn0  7450  ctssdc  7453  enumct  7455  nnnninf  7466  nnnninfeq  7468  nninfisollemne  7471  nninfisol  7473  finomni  7480  exmidlpo  7483  pr2cv1  7541  acneq  7558  finacn  7560  acfun  7563  exmidontriimlem3  7579  exmidontriimlem4  7580  pw1ne1  7588  onntri35  7596  exmidapne  7626  ccfunen  7630  cc2lem  7632  elni2  7681  recexnq  7757  recmulnqg  7758  enq0enq  7798  enq0sym  7799  enq0ref  7800  enq0tr  7801  enq0breq  7803  nqnq0pi  7805  nqnq0  7808  prop  7842  prcdnql  7851  prcunqu  7852  prubl  7853  prltlu  7854  prnmaxl  7855  prnminu  7856  prdisj  7859  prarloc  7870  genipv  7876  genpelvl  7879  genpelvu  7880  genprndl  7888  genprndu  7889  distrlem5prl  7953  distrlem5pru  7954  ltexprlemm  7967  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemm  8035  caucvgprlemladdfu  8044  caucvgprprlemmu  8062  elreal2  8197  ltresr  8206  axcnre  8248  axpre-suploclemres  8268  0re  8326  renepnf  8373  renemnf  8374  ltxrlt  8391  eqlei2  8421  0cnALT  8517  sup3exmid  9289  nn1suc  9325  nnne0  9334  xnn0xr  9639  nn0nepnf  9642  elz  9650  elnn0z  9661  elz2  9720  uzind4s  9999  elnn1uz2  10016  qre  10034  elpqb  10060  xnn0lenn0nn0  10277  xsubge0  10293  xposdif  10294  xleaddadd  10299  fzsn  10482  fz1sbc  10513  elfzp12  10516  fzm1  10517  fz01or  10528  fvinim0ffz  10670  suprzubdc  10681  zsupssdc  10683  xqltnle  10712  flqidz  10734  ceilqidz  10766  modqmuladdnn0  10818  frec2uzrand  10855  frecuzrdgtcl  10862  fzfig  10880  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  monoord  10935  seq3split  10938  seqsplitg  10939  iseqf1olemqval  10950  seq3id2  10976  seqhomog  10980  1exp  11018  bcval  11201  hashennn  11233  hashfibc  11297  zfz1isolem1  11306  zfz1iso  11307  seq3coll  11308  iswrdiz  11325  0wrd0  11344  lswlgt0cl  11371  ccatval1  11379  ccatval2  11380  ccatalpha  11395  ccatrcl1  11396  wrdl1s1  11412  ccats1val2  11422  wrd2ind  11509  pfxccatin12lem3  11518  pfxccatid  11527  reuccatpfxs1lem  11532  shftlem  11595  shftfibg  11599  shftfib  11602  shftfn  11603  2shfti  11610  rexuz3  11770  sqrt0rlem  11783  cau3  11896  negfi  12009  sumdc  12140  sumrbdclem  12160  summodclem2a  12164  fisumss  12175  prodrbdclem  12354  prodmodclem2a  12359  fprodssdc  12373  fprodsplit1f  12417  ef0lem  12443  odd2np1  12656  even2n  12657  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  nn0enne  12685  divalgmod  12710  uzwodc  12830  lcmgcdlem  12871  cncongr1  12897  1nprm  12908  isprm2  12911  dvdsnprmd  12919  prmdc  12924  exprmfct  12933  nprmdvds1  12935  coprm  12939  prmdiveq  13034  prm23lt5  13062  pcpre1  13091  pc2dvds  13129  pcz  13131  pcmpt  13142  qexpz  13151  4sqlem2  13188  4sqlem19  13208  prmlem0  13240  ballotfilem2  13277  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemhom  13355  ctiunctlemudc  13377  ssnnctlemct  13386  nninfdclemcl  13388  imasaddfnlemg  13684  ismgmid  13746  isgrpid2  13894  mhmlem  13966  eqgval  14075  dvdsrcl2  14455  nzrunit  14544  lringuplu  14552  dvdsrzring  14987  znrrg  15044  mplsubgfilemm  15138  fiinopn  15154  istopon  15163  basis2  15198  eltg3  15207  tg2  15210  tgidm  15224  bastop  15225  bastop2  15234  topnex  15236  isopn3  15275  tgrest  15319  cnpval  15348  lmbr  15363  cnconst  15384  txbas  15408  uptx  15424  txdis1cn  15428  cnmpt12  15437  cnmpt22  15444  hmeocnvb  15468  xblm  15567  isxms2  15602  mopni  15632  blssioo  15703  dedekindeulemuub  15767  dedekindeulemeu  15772  dedekindicclemuub  15776  dedekindicclemeu  15781  ivthinclemlm  15784  ivthinclemum  15785  ivthreinc  15795  pellexlem3  16150  bposlem5  16213  lgsfvalg  16222  lgsval2lem  16227  lgsdir2lem2  16246  gausslemma2dlem1a  16275  gausslemma2dlem4  16281  gausslemma2dlem6  16284  2lgslem1b  16306  2lgs  16321  2lgsoddprmlem2  16323  2lgsoddprmlem3  16328  2sqlem2  16332  2sqlem6  16337  2sqlem7  16338  2sqlem10  16342  vtxvalg  16355  iedgvalg  16356  umgredg  16484  upgrpredgv  16485  usgredg2vlem2  16562  ushgredgedg  16565  ushgredgedgloop  16567  griedg0ssusgr  16590  uhgrspansubgrlem  16615  vtxdgfifival  16630  iswlk  16662  upgrwlkvtxedg  16703  isclwwlknx  16755  clwwlkn1loopb  16759  clwwlknonex2lem1  16776  elabgf0  16903  bj-rspgt  16912  cbvrald  16914  decidi  16921  sumdc2  16925  bdssex  17026  bj-inex  17031  bj-intnexr  17033  bj-unexg  17045  bj-d0clsepcl  17049  bj-nnelirr  17077  bj-nn0suc  17088  bj-inf2vnlem1  17094  bj-inf2vnlem2  17095  bj-inf2vnlem3  17096  bj-inf2vnlem4  17097  bj-nn0sucALT  17102  bj-findis  17103  3dom  17116  wexmiddiffilem  17141  wexmiddifxy  17144  trilpolemcl  17184