Theorem eleq1 2073

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 2022	. . . 4 ⊢ (A = B → (x = A ↔ x = B))
2	1	anbi1d 438	. . 3 ⊢ (A = B → ((x = A ∧ x ∈ 𝐶) ↔ (x = B ∧ x ∈ 𝐶)))
3	2	exbidv 1679	. 2 ⊢ (A = B → (∃x(x = A ∧ x ∈ 𝐶) ↔ ∃x(x = B ∧ x ∈ 𝐶)))
4		df-clel 2009	. 2 ⊢ (A ∈ 𝐶 ↔ ∃x(x = A ∧ x ∈ 𝐶))
5		df-clel 2009	. 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 1223  ∃wex 1354   ∈ wcel 1366

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 1309  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-4 1373  ax-17 1392  ax-ial 1400  ax-ext 1995

This theorem depends on definitions:  df-bi 110  df-cleq 2006  df-clel 2009

This theorem is referenced by:  eleq12  2075  eleq1i  2076  eleq1d  2079  eleq1a  2082  cleqh  2110  nelneq  2111  clelsb3  2115  nfcjust  2139  cleqf  2174  nelne2  2265  neleq1  2270  rgen2a  2344  cbvralf  2496  cbvrexf  2497  cbvreu  2500  cbvrab  2524  ceqsralt  2549  vtoclgaf  2586  vtocl2gaf  2588  vtocl3gaf  2590  rspct  2617  rspc  2618  rspce  2619  ceqsrexv  2642  ceqsrexbv  2643  clel2  2645  elabgt  2652  elabgf  2653  elrabi  2663  elrabf  2664  elrab3t  2665  ralab2  2673  rexab2  2675  mo2icl  2688  morex  2693  reu2  2697  reu6  2698  rmo4  2702  reu8  2705  reuind  2712  nelrdva  2714  ru  2731  dfsbcq  2734  dfsbcq2  2735  sbc8g  2739  sbcel1gv  2789  rmob  2818  difjust  2887  unjust  2889  injust  2891  eldif  2895  dfss2f  2904  uniiunlem  2996  elun  3052  elin  3094  rabn0m  3213  disjne  3241  r19.3rm  3278  r19.9rmv  3281  raaanlem  3294  raaan  3295  elpwg  3331  elpr2  3358  elsnc2g  3368  rabsn  3400  tpid3g  3446  snssg  3463  difsn  3464  sssnm  3488  opeq1  3512  opeq2  3513  eluni  3546  elunii  3548  eluniab  3555  elint  3584  elintg  3586  elintab  3589  elintrabg  3591  intss1  3593  eliun  3624  eliin  3625  dfiunv2  3656  opabss  3784  cbvmpt  3814  trel  3824  trss  3826  ssex  3857  intnexr  3868  intexabim  3869  iinexgm  3871  euabex  3924  elopab  3958  opelopab2a  3965  ordelord  4056  onm  4076  ralxfr2d  4134  rexxfr2d  4135  rabxfrd  4139  reuhypd  4141  ordtriexmid  4182  ordtri2orexmid  4183  onsucsssucexmid  4184  onsucelsucexmid  4187  ordsucunielexmid  4188  regexmidlem1  4190  elirr  4196  sucprcreg  4199  en2lp  4204  ordsoexmid  4212  ordsuc  4213  tfis  4221  peano2  4233  findes  4241  limom  4251  opelxp  4289  opeliunxp  4310  opbrop  4334  ssrel  4343  ssrel2  4345  ssrelrel  4355  relopabi  4378  xpiindim  4388  eliunxp  4390  opeliunxp2  4391  ideqg  4402  dmmrnm  4469  dmxpm  4470  elreldm  4475  elrnmptg  4501  elres  4561  resiexg  4568  dfres2  4573  imai  4596  elimasng  4608  issref  4622  xpmlem  4659  xpm  4660  elxp4  4723  elxp5  4724  unielrel  4760  relcnvexb  4772  cnviinm  4774  dmfex  4992  funfveu  5101  funimass4  5137  fvelimab  5142  ssimaex  5147  fvopab3g  5158  fvopab3ig  5159  fvmptssdm  5168  chfnrn  5191  fvelrn  5211  fmpt  5232  ffnfv  5236  fmptco  5243  elunirn  5318  f1elima  5325  cbvriota  5390  acexmidlemab  5418  acexmidlemcase  5419  cbvmpt2x  5493  eloprabga  5502  resoprab  5508  elrnmpt2  5525  ov  5531  ovig  5533  ov6g  5549  ovg  5550  ovelrn  5560  caovimo  5605  fo1stresm  5699  fo2ndresm  5700  elxp6  5707  unielxp  5711  eqop2  5715  dfoprab4  5729  dfoprab4f  5730  fmpt2x  5737  1stconst  5753  2ndconst  5754  f1o2ndf1  5760  xporderlem  5762  dftpos3  5787  dftpos4  5788  tpostpos  5789  smoel  5825  frecsuc  5895  nntri3or  5975  nndcel  5979  iinerm  6077  riinerm  6078  th3qlem1  6107  elni2  6160  recexnq  6235  recmulnqg  6236  enq0enq  6272  enq0sym  6273  enq0ref  6274  enq0tr  6275  enq0breq  6277  nqnq0pi  6279  nqnq0  6282  prop  6315  prcdnql  6324  prcunqu  6325  prubl  6326  prltlu  6327  prnmaxl  6328  prnminu  6329  prdisj  6332  prarloc  6343  genipv  6349  genpelvl  6352  genpelvu  6353  genprndl  6362  genprndu  6363  distrlem5prl  6411  distrlem5pru  6412  ltexprlemm  6423  ltexprlemdisj  6429  ltexprlemloc  6430  ltexprlemrl  6433  ltexprlemru  6435  aptiprleml  6460  aptiprlemu  6461  elreal2  6537  ltresr  6545  axcnre  6570  0re  6628  renepnf  6673  renemnf  6674  ltxrlt  6685  eqlei2  6712  0cnALT  6801  nn1suc  7516  nnne0  7525  elz  7821  elnn0z  7832  qre  8042  elabgf0  8181  bj-rspgt  8190  cbvrald  8192  bdssex  8283  bj-inex  8288  bj-intnexr  8290  bj-unexg  8302  bj-d0clsepcl  8310  bj-nnelirr  8337  bj-nn0suc  8344  bj-inf2vnlem1  8350  bj-inf2vnlem2  8351  bj-inf2vnlem3  8352  bj-inf2vnlem4  8353  bj-nn0sucALT  8358  bj-findis  8359