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  6413  enq0sym  6414  enq0ref  6415  enq0tr  6416  enq0breq  6418  nqnq0pi  6420  nqnq0  6423  prop  6457  prcdnql  6466  prcunqu  6467  prubl  6468  prltlu  6469  prnmaxl  6470  prnminu  6471  prdisj  6474  prarloc  6485  genipv  6491  genpelvl  6494  genpelvu  6495  genprndl  6504  genprndu  6505  distrlem5prl  6560  distrlem5pru  6561  ltexprlemm  6572  ltexprlemdisj  6578  ltexprlemloc  6579  ltexprlemrl  6582  ltexprlemru  6584  aptiprleml  6609  aptiprlemu  6610  archpr  6613  elreal2  6688  ltresr  6696  axcnre  6725  0re  6785  renepnf  6830  renemnf  6831  ltxrlt  6842  eqlei2  6869  0cnALT  6958  nn1suc  7674  nnne0  7683  elz  7983  elnn0z  7994  elz2  8048  uzind4s  8269  elnn1uz2  8280  qre  8296  fzsn  8659  fz1sbc  8688  elfzp12  8691  fzm1  8692  frec2uzrand  8832  frecuzrdgfn  8839  fzfig  8847  iseqfveq2  8865  1exp  8898  elabgf0  9185  bj-rspgt  9194  cbvrald  9196  bdssex  9287  bj-inex  9292  bj-intnexr  9294  bj-unexg  9306  bj-d0clsepcl  9314  bj-nnelirr  9341  bj-nn0suc  9348  bj-inf2vnlem1  9354  bj-inf2vnlem2  9355  bj-inf2vnlem3  9356  bj-inf2vnlem4  9357  bj-nn0sucALT  9362  bj-findis  9363