Theorem eleq1 2078

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 2027	. . . 4 ⊢ (A = B → (x = A ↔ x = B))
2	1	anbi1d 441	. . 3 ⊢ (A = B → ((x = A ∧ x ∈ 𝐶) ↔ (x = B ∧ x ∈ 𝐶)))
3	2	exbidv 1684	. 2 ⊢ (A = B → (∃x(x = A ∧ x ∈ 𝐶) ↔ ∃x(x = B ∧ x ∈ 𝐶)))
4		df-clel 2014	. 2 ⊢ (A ∈ 𝐶 ↔ ∃x(x = A ∧ x ∈ 𝐶))
5		df-clel 2014	. 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 1226  ∃wex 1358   ∈ wcel 1370

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 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-4 1377  ax-17 1396  ax-ial 1405  ax-ext 2000

This theorem depends on definitions:  df-bi 110  df-cleq 2011  df-clel 2014

This theorem is referenced by:  eleq12  2080  eleq1i  2081  eleq1d  2084  eleq1a  2087  cleqh  2115  nelneq  2116  clelsb3  2120  nfcjust  2144  cleqf  2179  nelne2  2270  neleq1  2275  rgen2a  2349  cbvralf  2501  cbvrexf  2502  cbvreu  2505  cbvrab  2529  ceqsralt  2554  vtoclgaf  2591  vtocl2gaf  2593  vtocl3gaf  2595  rspct  2622  rspc  2623  rspce  2624  ceqsrexv  2647  ceqsrexbv  2648  clel2  2650  elabgt  2657  elabgf  2658  elrabi  2668  elrabf  2669  elrab3t  2670  ralab2  2678  rexab2  2680  mo2icl  2693  morex  2698  reu2  2702  reu6  2703  rmo4  2707  reu8  2710  reuind  2717  nelrdva  2719  ru  2736  dfsbcq  2739  dfsbcq2  2740  sbc8g  2744  sbcel1gv  2794  rmob  2823  difjust  2892  unjust  2894  injust  2896  eldif  2900  dfss2f  2909  uniiunlem  3001  elun  3057  elin  3099  rabn0m  3218  disjne  3246  r19.3rm  3285  r19.9rmv  3287  raaanlem  3301  raaan  3302  elpwg  3338  elpr2  3365  elsnc2g  3375  rabsn  3407  tpid3g  3453  snssg  3470  difsn  3471  sssnm  3495  opeq1  3519  opeq2  3520  eluni  3553  elunii  3555  eluniab  3562  elint  3591  elintg  3593  elintab  3596  elintrabg  3598  intss1  3600  eliun  3631  eliin  3632  dfiunv2  3663  opabss  3791  cbvmpt  3821  trel  3831  trss  3833  ssex  3864  intnexr  3875  intexabim  3876  iinexgm  3878  euabex  3931  elopab  3965  opelopab2a  3972  ordelord  4063  onm  4083  ralxfr2d  4142  rexxfr2d  4143  rabxfrd  4147  reuhypd  4149  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  onsucelsucexmid  4195  ordsucunielexmid  4196  regexmidlem1  4198  elirr  4204  sucprcreg  4207  en2lp  4212  ordsoexmid  4220  ordsuc  4221  tfis  4229  peano2  4241  findes  4249  limom  4259  opelxp  4297  opeliunxp  4318  opbrop  4342  ssrel  4351  ssrel2  4353  ssrelrel  4363  relopabi  4386  xpiindim  4396  eliunxp  4398  opeliunxp2  4399  ideqg  4410  dmmrnm  4477  dmxpm  4478  elreldm  4483  elrnmptg  4509  elres  4569  resiexg  4576  dfres2  4581  imai  4604  elimasng  4616  issref  4630  xpmlem  4667  xpm  4668  elxp4  4731  elxp5  4732  unielrel  4768  relcnvexb  4780  cnviinm  4782  dmfex  5000  funfveu  5109  funimass4  5145  fvelimab  5150  ssimaex  5155  fvopab3g  5166  fvopab3ig  5167  fvmptssdm  5176  chfnrn  5199  fvelrn  5219  fmpt  5240  ffnfv  5244  fmptco  5251  elunirn  5326  f1elima  5333  cbvriota  5398  acexmidlemab  5426  acexmidlemcase  5427  cbvmpt2x  5501  eloprabga  5510  resoprab  5516  elrnmpt2  5533  ov  5539  ovig  5541  ov6g  5557  ovg  5558  ovelrn  5568  caovimo  5613  fo1stresm  5707  fo2ndresm  5708  elxp6  5715  unielxp  5719  eqop2  5723  dfoprab4  5737  dfoprab4f  5738  fmpt2x  5745  1stconst  5761  2ndconst  5762  f1o2ndf1  5768  xporderlem  5770  dftpos3  5795  dftpos4  5796  tpostpos  5797  smoel  5833  frecsuc  5903  nntri3or  5983  nndcel  5987  iinerm  6085  riinerm  6086  th3qlem1  6115  elni2  6168  recex  6243  recmulnqg  6244  enq0enq  6280  enq0sym  6281  enq0ref  6282  enq0tr  6283  enq0breq  6285  nqnq0pi  6287  nqnq0  6290  prop  6323  prcdnql  6332  prcunqu  6333  prubl  6334  prltlu  6335  prnmaxl  6336  prnminu  6337  prdisj  6340  prarloc  6351  genipv  6357  genpelvl  6360  genpelvu  6361  genprndl  6370  genprndu  6371  distrlem5prl  6419  distrlem5pru  6420  ltexprlemm  6431  ltexprlemdisj  6437  ltexprlemloc  6438  ltexprlemrl  6441  ltexprlemru  6443  elreal2  6536  ltresr  6544  axcnre  6569  0re  6623  renepnf  6668  renemnf  6669  ltxrlt  6680  eqlei2  6704  0cnALT  6788  elabgf0  7162  bj-rspgt  7171  cbvrald  7173  bdssex  7264  bj-inex  7269  bj-intnexr  7271  bj-unexg  7283  bj-d0clsepcl  7287  bj-nnelirr  7314  bj-nn0suc  7321  bj-inf2vnlem1  7327  bj-inf2vnlem2  7328  bj-inf2vnlem3  7329  bj-inf2vnlem4  7330  bj-nn0sucALT  7335  bj-findis  7336