Theorem eleq1 2100

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

Assertion

Ref	Expression
eleq1	⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Proof of Theorem eleq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqeq2 2049	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 438	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1706	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2036	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2036	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 212	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243  ∃wex 1381   ∈ wcel 1393

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022

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

This theorem is referenced by:  eleq12  2102  eleq1i  2103  eleq1d  2106  eleq1a  2109  cleqh  2137  nelneq  2138  clelsb3  2142  nfcjust  2166  cleqf  2201  nelne2  2296  neleq1  2301  rgen2a  2375  cbvralf  2527  cbvrexf  2528  cbvreu  2531  cbvrab  2555  eqvisset  2565  ceqsralt  2581  vtoclgaf  2618  vtocl2gaf  2620  vtocl3gaf  2622  rspct  2649  rspc  2650  rspce  2651  ceqsrexv  2674  ceqsrexbv  2675  clel2  2677  elabgt  2684  elabgf  2685  elrabi  2695  elrabf  2696  elrab3t  2697  ralab2  2705  rexab2  2707  mo2icl  2720  morex  2725  reu2  2729  reu6  2730  rmo4  2734  reu8  2737  reuind  2744  nelrdva  2746  ru  2763  dfsbcq  2766  dfsbcq2  2767  sbc8g  2771  sbcel1gv  2821  rmob  2850  difjust  2919  unjust  2921  injust  2923  eldif  2927  dfss2f  2936  uniiunlem  3028  elun  3084  elin  3126  rabn0m  3245  disjne  3273  r19.3rm  3310  r19.9rmv  3313  raaanlem  3326  raaan  3327  elpwg  3367  elpr2  3397  elsn2g  3404  rabsn  3437  tpid3g  3483  snssg  3500  difsn  3501  sssnm  3525  opeq1  3549  opeq2  3550  eluni  3583  elunii  3585  eluniab  3592  elint  3621  elintg  3623  elintab  3626  elintrabg  3628  intss1  3630  eliun  3661  eliin  3662  dfiunv2  3693  opabss  3821  cbvmpt  3851  trel  3861  trss  3863  ssex  3894  intnexr  3905  intexabim  3906  iinexgm  3908  euabex  3961  elopab  3995  opelopab2a  4002  frirrg  4087  tz7.2  4091  ordelord  4118  onm  4138  ralxfr2d  4196  rexxfr2d  4197  rabxfrd  4201  reuhypd  4203  ordtriexmid  4247  ordtri2orexmid  4248  ontr2exmid  4250  onsucsssucexmid  4252  onsucelsucexmid  4255  ordsucunielexmid  4256  regexmidlem1  4258  elirr  4266  nordeq  4268  sucprcreg  4273  en2lp  4278  ordsoexmid  4286  ordsuc  4287  onsucuni2  4288  tfis  4306  peano2  4318  findes  4326  limom  4336  opelxp  4374  opeliunxp  4395  opbrop  4419  ssrel  4428  ssrel2  4430  ssrelrel  4440  relopabi  4463  xpiindim  4473  eliunxp  4475  opeliunxp2  4476  ideqg  4487  dmmrnm  4554  dmxpm  4555  elreldm  4560  elrnmptg  4586  elres  4646  resiexg  4653  dfres2  4658  imai  4681  elimasng  4693  issref  4707  xpmlem  4744  xpm  4745  elxp4  4808  elxp5  4809  unielrel  4845  relcnvexb  4857  cnviinm  4859  dmfex  5079  funfveu  5188  funimass4  5224  fvelimab  5229  ssimaex  5234  fvopab3g  5245  fvopab3ig  5246  fvmptssdm  5255  chfnrn  5278  fvelrn  5298  fmpt  5319  ffnfv  5323  fmptco  5330  elunirn  5405  f1elima  5412  cbvriota  5478  acexmidlemab  5506  acexmidlemcase  5507  cbvmpt2x  5582  eloprabga  5591  resoprab  5597  elrnmpt2  5614  ov  5620  ovig  5622  ov6g  5638  ovg  5639  ovelrn  5649  caovimo  5694  fo1stresm  5788  fo2ndresm  5789  elxp6  5796  unielxp  5800  eqop2  5804  dfoprab4  5818  dfoprab4f  5819  fmpt2x  5826  1stconst  5842  2ndconst  5843  f1o2ndf1  5849  xporderlem  5852  dftpos3  5877  dftpos4  5878  tpostpos  5879  smoel  5915  frecsuc  5991  freccl  5993  nntri3or  6072  nntri3  6075  nndcel  6078  iinerm  6178  riinerm  6179  th3qlem1  6208  dom2lem  6252  fiprc  6292  xpsnen  6295  phplem3g  6319  phpelm  6328  ssfiexmid  6336  snon0  6356  ordiso2  6357  elni2  6412  recexnq  6488  recmulnqg  6489  enq0enq  6529  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0breq  6534  nqnq0pi  6536  nqnq0  6539  prop  6573  prcdnql  6582  prcunqu  6583  prubl  6584  prltlu  6585  prnmaxl  6586  prnminu  6587  prdisj  6590  prarloc  6601  genipv  6607  genpelvl  6610  genpelvu  6611  genprndl  6619  genprndu  6620  distrlem5prl  6684  distrlem5pru  6685  ltexprlemm  6698  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  aptiprleml  6737  aptiprlemu  6738  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemm  6766  caucvgprlemladdfu  6775  caucvgprprlemmu  6793  elreal2  6907  ltresr  6915  axcnre  6955  0re  7027  renepnf  7073  renemnf  7074  ltxrlt  7085  eqlei2  7112  0cnALT  7201  nn1suc  7933  nnne0  7942  elz  8247  elnn0z  8258  elz2  8312  uzind4s  8533  elnn1uz2  8544  qre  8560  fzsn  8929  fz1sbc  8958  elfzp12  8961  fzm1  8962  fvinim0ffz  9096  flqidz  9128  ceilqidz  9158  frec2uzrand  9191  frecuzrdgfn  9198  fzfig  9206  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  1exp  9284  shftlem  9417  shftfibg  9421  shftfib  9424  shftfn  9425  2shfti  9432  rexuz3  9588  sqrt0rlem  9601  cau3  9711  elabgf0  9916  bj-rspgt  9925  cbvrald  9927  bdssex  10022  bj-inex  10027  bj-intnexr  10029  bj-unexg  10041  bj-d0clsepcl  10049  bj-nnelirr  10078  bj-nn0suc  10089  bj-inf2vnlem1  10095  bj-inf2vnlem2  10096  bj-inf2vnlem3  10097  bj-inf2vnlem4  10098  bj-nn0sucALT  10103  bj-findis  10104