Theorem eleq1 2097

Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eleq1	⊢ (A = B → (A ∈ 𝐶 ↔ B ∈ 𝐶))

Proof of Theorem eleq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2046	. . . 4 ⊢ (A = B → (x = A ↔ x = B))
2	1	anbi1d 438	. . 3 ⊢ (A = B → ((x = A ∧ x ∈ 𝐶) ↔ (x = B ∧ x ∈ 𝐶)))
3	2	exbidv 1703	. 2 ⊢ (A = B → (∃x(x = A ∧ x ∈ 𝐶) ↔ ∃x(x = B ∧ x ∈ 𝐶)))
4		df-clel 2033	. 2 ⊢ (A ∈ 𝐶 ↔ ∃x(x = A ∧ x ∈ 𝐶))
5		df-clel 2033	. 2 ⊢ (B ∈ 𝐶 ↔ ∃x(x = B ∧ x ∈ 𝐶))
6	3, 4, 5	3bitr4g 212	1 ⊢ (A = B → (A ∈ 𝐶 ↔ B ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-clel 2033

This theorem is referenced by:  eleq12  2099  eleq1i  2100  eleq1d  2103  eleq1a  2106  cleqh  2134  nelneq  2135  clelsb3  2139  nfcjust  2163  cleqf  2198  nelne2  2290  neleq1  2295  rgen2a  2369  cbvralf  2521  cbvrexf  2522  cbvreu  2525  cbvrab  2549  eqvisset  2559  ceqsralt  2575  vtoclgaf  2612  vtocl2gaf  2614  vtocl3gaf  2616  rspct  2643  rspc  2644  rspce  2645  ceqsrexv  2668  ceqsrexbv  2669  clel2  2671  elabgt  2678  elabgf  2679  elrabi  2689  elrabf  2690  elrab3t  2691  ralab2  2699  rexab2  2701  mo2icl  2714  morex  2719  reu2  2723  reu6  2724  rmo4  2728  reu8  2731  reuind  2738  nelrdva  2740  ru  2757  dfsbcq  2760  dfsbcq2  2761  sbc8g  2765  sbcel1gv  2815  rmob  2844  difjust  2913  unjust  2915  injust  2917  eldif  2921  dfss2f  2930  uniiunlem  3022  elun  3078  elin  3120  rabn0m  3239  disjne  3267  r19.3rm  3304  r19.9rmv  3307  raaanlem  3320  raaan  3321  elpwg  3359  elpr2  3386  elsnc2g  3396  rabsn  3428  tpid3g  3474  snssg  3491  difsn  3492  sssnm  3516  opeq1  3540  opeq2  3541  eluni  3574  elunii  3576  eluniab  3583  elint  3612  elintg  3614  elintab  3617  elintrabg  3619  intss1  3621  eliun  3652  eliin  3653  dfiunv2  3684  opabss  3812  cbvmpt  3842  trel  3852  trss  3854  ssex  3885  intnexr  3896  intexabim  3897  iinexgm  3899  euabex  3952  elopab  3986  opelopab2a  3993  ordelord  4084  onm  4104  ralxfr2d  4162  rexxfr2d  4163  rabxfrd  4167  reuhypd  4169  ordtriexmid  4210  ordtri2orexmid  4211  onsucsssucexmid  4212  onsucelsucexmid  4215  ordsucunielexmid  4216  regexmidlem1  4218  elirr  4224  sucprcreg  4227  en2lp  4232  ordsoexmid  4240  ordsuc  4241  tfis  4249  peano2  4261  findes  4269  limom  4279  opelxp  4317  opeliunxp  4338  opbrop  4362  ssrel  4371  ssrel2  4373  ssrelrel  4383  relopabi  4406  xpiindim  4416  eliunxp  4418  opeliunxp2  4419  ideqg  4430  dmmrnm  4497  dmxpm  4498  elreldm  4503  elrnmptg  4529  elres  4589  resiexg  4596  dfres2  4601  imai  4624  elimasng  4636  issref  4650  xpmlem  4687  xpm  4688  elxp4  4751  elxp5  4752  unielrel  4788  relcnvexb  4800  cnviinm  4802  dmfex  5022  funfveu  5131  funimass4  5167  fvelimab  5172  ssimaex  5177  fvopab3g  5188  fvopab3ig  5189  fvmptssdm  5198  chfnrn  5221  fvelrn  5241  fmpt  5262  ffnfv  5266  fmptco  5273  elunirn  5348  f1elima  5355  cbvriota  5421  acexmidlemab  5449  acexmidlemcase  5450  cbvmpt2x  5524  eloprabga  5533  resoprab  5539  elrnmpt2  5556  ov  5562  ovig  5564  ov6g  5580  ovg  5581  ovelrn  5591  caovimo  5636  fo1stresm  5730  fo2ndresm  5731  elxp6  5738  unielxp  5742  eqop2  5746  dfoprab4  5760  dfoprab4f  5761  fmpt2x  5768  1stconst  5784  2ndconst  5785  f1o2ndf1  5791  xporderlem  5793  dftpos3  5818  dftpos4  5819  tpostpos  5820  smoel  5856  frecsuc  5930  freccl  5932  nntri3or  6011  nntri3  6014  nndcel  6016  iinerm  6114  riinerm  6115  th3qlem1  6144  dom2lem  6188  fiprc  6228  xpsnen  6231  ssfiexmid  6254  elni2  6298  recexnq  6374  recmulnqg  6375  enq0enq  6414  enq0sym  6415  enq0ref  6416  enq0tr  6417  enq0breq  6419  nqnq0pi  6421  nqnq0  6424  prop  6458  prcdnql  6467  prcunqu  6468  prubl  6469  prltlu  6470  prnmaxl  6471  prnminu  6472  prdisj  6475  prarloc  6486  genipv  6492  genpelvl  6495  genpelvu  6496  genprndl  6504  genprndu  6505  distrlem5prl  6562  distrlem5pru  6563  ltexprlemm  6574  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  aptiprleml  6611  aptiprlemu  6612  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemm  6639  caucvgprlemladdfu  6648  elreal2  6728  ltresr  6736  axcnre  6765  0re  6825  renepnf  6870  renemnf  6871  ltxrlt  6882  eqlei2  6909  0cnALT  6998  nn1suc  7714  nnne0  7723  elz  8023  elnn0z  8034  elz2  8088  uzind4s  8309  elnn1uz2  8320  qre  8336  fzsn  8699  fz1sbc  8728  elfzp12  8731  fzm1  8732  frec2uzrand  8872  frecuzrdgfn  8879  fzfig  8887  iseqfveq2  8905  1exp  8938  sqrt0rlem  9212  elabgf0  9251  bj-rspgt  9260  cbvrald  9262  bdssex  9357  bj-inex  9362  bj-intnexr  9364  bj-unexg  9376  bj-d0clsepcl  9384  bj-nnelirr  9413  bj-nn0suc  9424  bj-inf2vnlem1  9430  bj-inf2vnlem2  9431  bj-inf2vnlem3  9432  bj-inf2vnlem4  9433  bj-nn0sucALT  9438  bj-findis  9439