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  7376  ctssdclemn0  7451  ctssdc  7454  enumct  7456  nnnninf  7467  nnnninfeq  7469  nninfisollemne  7472  nninfisol  7474  finomni  7481  exmidlpo  7484  pr2cv1  7542  acneq  7559  finacn  7561  acfun  7564  exmidontriimlem3  7580  exmidontriimlem4  7581  pw1ne1  7589  onntri35  7597  exmidapne  7627  ccfunen  7631  cc2lem  7633  elni2  7682  recexnq  7758  recmulnqg  7759  enq0enq  7799  enq0sym  7800  enq0ref  7801  enq0tr  7802  enq0breq  7804  nqnq0pi  7806  nqnq0  7809  prop  7843  prcdnql  7852  prcunqu  7853  prubl  7854  prltlu  7855  prnmaxl  7856  prnminu  7857  prdisj  7860  prarloc  7871  genipv  7877  genpelvl  7880  genpelvu  7881  genprndl  7889  genprndu  7890  distrlem5prl  7954  distrlem5pru  7955  ltexprlemm  7968  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  aptiprleml  8007  aptiprlemu  8008  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemm  8036  caucvgprlemladdfu  8045  caucvgprprlemmu  8063  elreal2  8198  ltresr  8207  axcnre  8249  axpre-suploclemres  8269  0re  8327  renepnf  8374  renemnf  8375  ltxrlt  8392  eqlei2  8422  0cnALT  8518  sup3exmid  9290  nn1suc  9326  nnne0  9335  xnn0xr  9640  nn0nepnf  9643  elz  9651  elnn0z  9662  elz2  9721  uzind4s  10000  elnn1uz2  10017  qre  10035  elpqb  10061  xnn0lenn0nn0  10278  xsubge0  10294  xposdif  10295  xleaddadd  10300  fzsn  10483  fz1sbc  10514  elfzp12  10517  fzm1  10518  fz01or  10529  fvinim0ffz  10671  suprzubdc  10682  zsupssdc  10684  xqltnle  10713  flqidz  10736  ceilqidz  10768  modqmuladdnn0  10820  frec2uzrand  10857  frecuzrdgtcl  10864  fzfig  10882  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  monoord  10937  seq3split  10940  seqsplitg  10941  iseqf1olemqval  10952  seq3id2  10978  seqhomog  10982  1exp  11020  bcval  11203  hashennn  11235  hashfibc  11299  zfz1isolem1  11308  zfz1iso  11309  seq3coll  11310  iswrdiz  11327  0wrd0  11346  lswlgt0cl  11373  ccatval1  11381  ccatval2  11382  ccatalpha  11397  ccatrcl1  11398  wrdl1s1  11414  ccats1val2  11424  wrd2ind  11511  pfxccatin12lem3  11520  pfxccatid  11529  reuccatpfxs1lem  11534  shftlem  11597  shftfibg  11601  shftfib  11604  shftfn  11605  2shfti  11612  rexuz3  11772  sqrt0rlem  11785  cau3  11898  negfi  12011  sumdc  12143  sumrbdclem  12163  summodclem2a  12167  fisumss  12178  prodrbdclem  12357  prodmodclem2a  12362  fprodssdc  12376  fprodsplit1f  12420  ef0lem  12446  odd2np1  12659  even2n  12660  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  nn0enne  12688  divalgmod  12713  uzwodc  12833  lcmgcdlem  12874  cncongr1  12900  1nprm  12911  isprm2  12914  dvdsnprmd  12922  prmdc  12927  exprmfct  12936  nprmdvds1  12938  coprm  12942  prmdiveq  13037  prm23lt5  13065  pcpre1  13094  pc2dvds  13132  pcz  13134  pcmpt  13145  qexpz  13154  4sqlem2  13191  4sqlem19  13211  prmlem0  13243  ballotfilem2  13280  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemhom  13358  ctiunctlemudc  13380  ssnnctlemct  13389  nninfdclemcl  13391  imasaddfnlemg  13688  ismgmid  13750  isgrpid2  13898  mhmlem  13970  eqgval  14079  dvdsrcl2  14490  nzrunit  14579  lringuplu  14587  dvdsrzring  15022  znrrg  15079  mplsubgfilemm  15180  fiinopn  15196  istopon  15205  basis2  15240  eltg3  15249  tg2  15252  tgidm  15266  bastop  15267  bastop2  15276  topnex  15278  isopn3  15317  tgrest  15361  cnpval  15390  lmbr  15405  cnconst  15426  txbas  15450  uptx  15466  txdis1cn  15470  cnmpt12  15479  cnmpt22  15486  hmeocnvb  15510  xblm  15609  isxms2  15644  mopni  15674  blssioo  15745  dedekindeulemuub  15809  dedekindeulemeu  15814  dedekindicclemuub  15818  dedekindicclemeu  15823  ivthinclemlm  15826  ivthinclemum  15827  ivthreinc  15837  pellexlem3  16192  bposlem5  16276  lgsfvalg  16290  lgsval2lem  16295  lgsdir2lem2  16314  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  gausslemma2dlem6  16352  2lgslem1b  16374  2lgs  16389  2lgsoddprmlem2  16391  2lgsoddprmlem3  16396  2sqlem2  16400  2sqlem6  16405  2sqlem7  16406  2sqlem10  16410  vtxvalg  16423  iedgvalg  16424  umgredg  16552  upgrpredgv  16553  usgredg2vlem2  16630  ushgredgedg  16633  ushgredgedgloop  16635  griedg0ssusgr  16658  uhgrspansubgrlem  16683  vtxdgfifival  16698  iswlk  16730  upgrwlkvtxedg  16771  isclwwlknx  16823  clwwlkn1loopb  16827  clwwlknonex2lem1  16844  elabgf0  16971  bj-rspgt  16980  cbvrald  16982  decidi  16989  sumdc2  16993  bdssex  17094  bj-inex  17099  bj-intnexr  17101  bj-unexg  17113  bj-d0clsepcl  17117  bj-nnelirr  17145  bj-nn0suc  17156  bj-inf2vnlem1  17162  bj-inf2vnlem2  17163  bj-inf2vnlem3  17164  bj-inf2vnlem4  17165  bj-nn0sucALT  17170  bj-findis  17171  3dom  17184  wexmiddiffilem  17209  wexmiddifxy  17212  trilpolemcl  17253