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  6503  genprndu  6504  distrlem5prl  6561  distrlem5pru  6562  ltexprlemm  6573  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  aptiprleml  6610  aptiprlemu  6611  archpr  6614  cauappcvgprlemm  6616  cauappcvgprlemladdfu  6625  cauappcvgprlemladdfl  6626  elreal2  6708  ltresr  6716  axcnre  6745  0re  6805  renepnf  6850  renemnf  6851  ltxrlt  6862  eqlei2  6889  0cnALT  6978  nn1suc  7694  nnne0  7703  elz  8003  elnn0z  8014  elz2  8068  uzind4s  8289  elnn1uz2  8300  qre  8316  fzsn  8679  fz1sbc  8708  elfzp12  8711  fzm1  8712  frec2uzrand  8852  frecuzrdgfn  8859  fzfig  8867  iseqfveq2  8885  1exp  8918  sqrt0rlem  9192  elabgf0  9231  bj-rspgt  9240  cbvrald  9242  bdssex  9333  bj-inex  9338  bj-intnexr  9340  bj-unexg  9352  bj-d0clsepcl  9360  bj-nnelirr  9387  bj-nn0suc  9394  bj-inf2vnlem1  9400  bj-inf2vnlem2  9401  bj-inf2vnlem3  9402  bj-inf2vnlem4  9403  bj-nn0sucALT  9408  bj-findis  9409