Theorem eleq1 2141

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 2090	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 = 𝐴 ↔ 𝑥 = 𝐵))
2	1	anbi1d 452	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ (𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
3	2	exbidv 1746	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶)))
4		df-clel 2077	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐶))
5		df-clel 2077	. 2 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝑥 ∈ 𝐶))
6	3, 4, 5	3bitr4g 221	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   = wceq 1284  ∃wex 1421   ∈ wcel 1433

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-clel 2077

This theorem is referenced by:  eleq12  2143  eleq1i  2144  eleq1d  2147  eleq1a  2150  cleqh  2178  nelneq  2179  clelsb3  2183  nfcjust  2207  cleqf  2242  nelne2  2336  neleq1  2343  rgen2a  2417  cbvralf  2571  cbvrexf  2572  cbvreu  2575  cbvrab  2599  eqvisset  2609  ceqsralt  2626  vtoclgaf  2663  vtocl2gaf  2665  vtocl3gaf  2667  rspct  2694  rspc  2695  rspce  2696  rspc2gv  2712  ceqsrexv  2725  ceqsrexbv  2726  clel2  2728  elabgt  2735  elabgf  2736  elrabi  2746  elrabf  2747  elrab3t  2748  ralab2  2756  rexab2  2758  mo2icl  2771  morex  2776  reu2  2780  reu6  2781  rmo4  2785  reu8  2788  reuind  2795  nelrdva  2797  ru  2814  dfsbcq  2817  dfsbcq2  2818  sbc8g  2822  sbcel1v  2876  rmob  2906  difjust  2974  unjust  2976  injust  2978  eldif  2982  dfss2f  2990  uniiunlem  3082  elun  3113  elin  3155  rabn0m  3272  disjne  3297  r19.3rm  3330  r19.9rmv  3333  raaanlem  3346  raaan  3347  elpwg  3390  elpr2  3420  elsn2g  3427  rabsn  3459  tpid3g  3505  snssg  3522  difsn  3523  sssnm  3546  opeq1  3570  opeq2  3571  eluni  3604  elunii  3606  eluniab  3613  elint  3642  elintg  3644  elintab  3647  elintrabg  3649  intss1  3651  eliun  3682  eliin  3683  dfiunv2  3714  opabss  3842  cbvmpt  3872  trel  3882  trss  3884  ssex  3915  intnexr  3926  intexabim  3927  iinexgm  3929  euabex  3980  elopab  4013  opelopab2a  4020  frirrg  4105  tz7.2  4109  ordelord  4136  onm  4156  ralxfr2d  4214  rexxfr2d  4215  rabxfrd  4219  reuhypd  4221  ordtriexmid  4265  ordtri2orexmid  4266  ontr2exmid  4268  onsucsssucexmid  4270  onsucelsucexmid  4273  ordsucunielexmid  4274  regexmidlem1  4276  elirr  4284  nordeq  4287  sucprcreg  4292  en2lp  4297  ordsoexmid  4305  ordsuc  4306  onsucuni2  4307  tfis  4324  peano2  4336  findes  4344  limom  4354  opelxp  4392  opeliunxp  4413  opbrop  4437  ssrel  4446  ssrel2  4448  ssrelrel  4458  relopabi  4481  xpiindim  4491  eliunxp  4493  opeliunxp2  4494  ideqg  4505  dmmrnm  4572  dmxpm  4573  elreldm  4578  elrnmptg  4604  elres  4664  resiexg  4673  dfres2  4678  imai  4701  elimasng  4713  issref  4727  xpmlem  4764  xpm  4765  elxp4  4828  elxp5  4829  unielrel  4865  relcnvexb  4877  cnviinm  4879  dmfex  5099  funfveu  5208  funimass4  5245  fvelimab  5250  ssimaex  5255  fvopab3g  5266  fvopab3ig  5267  fvmptssdm  5276  chfnrn  5299  fvelrn  5319  fmpt  5340  ffnfv  5344  fmptco  5351  elunirn  5426  f1elima  5433  cbvriota  5498  acexmidlemab  5526  acexmidlemcase  5527  cbvmpt2x  5602  eloprabga  5611  resoprab  5617  elrnmpt2  5634  ov  5640  ovig  5642  ov6g  5658  ovg  5659  ovelrn  5669  caovimo  5714  fo1stresm  5808  fo2ndresm  5809  elxp6  5816  unielxp  5820  eqop2  5824  dfoprab4  5838  dfoprab4f  5839  fmpt2x  5846  1stconst  5862  2ndconst  5863  f1o2ndf1  5869  xporderlem  5872  f1od2  5876  dftpos3  5900  dftpos4  5901  tpostpos  5902  smoel  5938  frecsuc  6014  freccl  6016  nntri3or  6095  nntri3  6098  nndcel  6101  iinerm  6201  riinerm  6202  th3qlem1  6231  dom2lem  6275  fiprc  6315  xpsnen  6318  phplem3g  6342  phpelm  6352  ssfiexmid  6361  domfiexmid  6363  snon0  6387  f1dmvrnfibi  6393  f1vrnfibi  6394  ordiso2  6446  elni2  6504  recexnq  6580  recmulnqg  6581  enq0enq  6621  enq0sym  6622  enq0ref  6623  enq0tr  6624  enq0breq  6626  nqnq0pi  6628  nqnq0  6631  prop  6665  prcdnql  6674  prcunqu  6675  prubl  6676  prltlu  6677  prnmaxl  6678  prnminu  6679  prdisj  6682  prarloc  6693  genipv  6699  genpelvl  6702  genpelvu  6703  genprndl  6711  genprndu  6712  distrlem5prl  6776  distrlem5pru  6777  ltexprlemm  6790  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  aptiprleml  6829  aptiprlemu  6830  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  caucvgprlemm  6858  caucvgprlemladdfu  6867  caucvgprprlemmu  6885  elreal2  6999  ltresr  7007  axcnre  7047  0re  7119  renepnf  7166  renemnf  7167  ltxrlt  7178  eqlei2  7205  0cnALT  7298  nn1suc  8058  nnne0  8067  elz  8353  elnn0z  8364  elz2  8419  uzind4s  8678  elnn1uz2  8694  qre  8710  fzsn  9084  fz1sbc  9113  elfzp12  9116  fzm1  9117  fvinim0ffz  9250  flqidz  9288  ceilqidz  9318  modqmuladdnn0  9370  frec2uzrand  9407  frecuzrdgfn  9414  fzfig  9422  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  1exp  9505  bcval  9676  shftlem  9704  shftfibg  9708  shftfib  9711  shftfn  9712  2shfti  9719  rexuz3  9876  sqrt0rlem  9889  cau3  10001  negfi  10110  odd2np1  10272  even2n  10273  fz01or  10278  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  nn0enne  10302  divalgmod  10327  lcmgcdlem  10459  cncongr1  10485  1nprm  10496  isprm2  10499  dvdsnprmd  10507  exprmfct  10519  nprmdvds1  10521  coprm  10523  elabgf0  10587  bj-rspgt  10596  cbvrald  10598  bdssex  10693  bj-inex  10698  bj-intnexr  10700  bj-unexg  10712  bj-d0clsepcl  10720  bj-nnelirr  10748  bj-nn0suc  10759  bj-inf2vnlem1  10765  bj-inf2vnlem2  10766  bj-inf2vnlem3  10767  bj-inf2vnlem4  10768  bj-nn0sucALT  10773  bj-findis  10774