Theorem eleq2d 2308

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
eleq2d	⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq2 2302	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  eleq12d  2309  eleqtrd  2317  neleqtrd  2336  neleqtrrd  2337  abeq2d  2351  eqabrd  2378  nfceqdf  2391  drnfc1  2409  drnfc2  2410  sbcbid  3109  cbvcsbw  3151  cbvcsb  3152  sbcel1g  3166  csbeq2d  3172  csbie2g  3198  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  rabsnif  3778  opeq1  3904  opeq2  3905  cbviun  4049  cbviin  4050  iinxsng  4086  iinxprg  4087  iunxsng  4088  iunxsngf  4090  cbvdisj  4116  disjnim  4120  disjiun  4125  mpteq12f  4211  axpweq  4308  rabxfrd  4615  onsucelsucexmid  4677  ordsucunielexmid  4678  0elsucexmid  4712  0nelelxp  4803  opeliunxp  4830  opeliunxp2  4920  iunxpf  4928  elrelimasn  5153  elimasng  5155  xpimasn  5236  ressn  5328  funfni  5483  fnbr  5485  fun11iun  5660  relndmfv  5728  fvelrnb  5750  foelcdmi  5755  fvun1  5769  fvco2  5774  elfvmptrab1  5801  elfvmptrab  5802  elpreima  5828  dff3im  5853  resflem  5872  fmptco  5874  funfvima3  5952  foima2  5957  eluniimadm  5971  dff13  5974  f1eqcocnv  5997  isoini  6024  riotaeqdv  6039  mpoeq123dva  6149  cbvmpox  6166  ovelrn  6238  elovmpod  6287  elovmpo  6288  elovmporab  6289  elovmporab1w  6290  fmpox  6436  disjxp1  6472  elsuppfng  6482  elsuppfn  6483  suppfnss  6497  suppcofn  6506  opeliunxp2f  6509  mpoxopn0yelv  6510  mpoxopovel  6512  rbropapd  6513  rntpos  6528  smoel  6571  smoiso  6573  smoel2  6574  tfrlem9  6590  tfrlemisucaccv  6596  tfrlemiubacc  6601  tfrlemi14d  6604  tfri2d  6607  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemubacc  6630  tfrcllemres  6633  rdgon  6657  freceq1  6663  freceq2  6664  frec0g  6668  frecabcl  6670  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecsuc  6678  nnsucelsuc  6764  nnsucuniel  6768  nnmordi  6789  ereldm  6852  iinerm  6881  elmapg  6935  elpmg  6938  elixpsn  7017  ixpsnf1o  7018  pw2f1odclem  7134  phplem4  7156  phplem3g  7157  phplem4on  7169  exmidpw  7215  fiintim  7238  fidcenumlemrks  7270  fidcenumlemrk  7271  elfi  7305  2omap  7319  ordiso2  7376  ctssdccl  7452  nnnninfeq  7469  cc2lem  7633  cc2  7634  cc3  7635  archnqq  7785  ltdfpr  7874  genpelxp  7879  genpelvl  7880  genpelvu  7881  addcanprleml  7982  addcanprlemu  7983  cauappcvgprlem1  8027  suplocexprlemell  8081  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemub  8091  suplocexprlemlub  8092  cnm  8200  indval0  9300  eluz1  9935  elixx1  10310  elioo2  10334  elfz1  10427  elfzp1  10490  fzpr  10495  fzsuc2  10497  fzrev3  10505  elfzp12  10517  fzm1  10518  fzoval  10566  elfzo  10567  fzodcel  10571  elfzom1b  10658  fzosplitsni  10665  nninfdcex  10683  zmodidfzo  10805  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seqf1og  10973  bcval  11203  bcpasc  11220  hashf1lem1  11301  fundm2domnop0  11316  wrdmap  11352  elovmpowrd  11362  ccatfvalfi  11376  elfzelfzccat  11384  ccatlid  11390  ccatass  11392  ccatrn  11393  ccatalpha  11397  swrdfv2  11451  ccatswrd  11458  swrdccat2  11459  pfxfv  11472  pfxeq  11484  ccatpfx  11489  swrdswrd  11493  swrdpfx  11495  pfxpfx  11496  cats1un  11509  swrdccatfn  11512  swrdccatin1  11513  pfxccatin12lem4  11514  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2c  11518  pfxccatin12lem2  11519  swrdccat3blem  11527  swrdccatin1d  11531  swrdccatin2d  11532  pfxccatin12d  11533  shftfn  11605  shftval  11606  seq3shft  11619  iser3shft  12131  sumeq1  12140  summodclem3  12166  summodclem2a  12167  isumss  12177  fsumsplit  12193  sumsplitdc  12218  fsum2dlemstep  12220  fisumcom2  12224  fsumparts  12256  explecnv  12291  fprodsplitdc  12382  fprodsplit  12383  fprod2dlemstep  12408  fprodcom2fi  12412  eftlub  12476  divalgmod  12713  bitsval  12729  bitsp1e  12738  bitsp1o  12739  algfx  12849  eucalgcvga  12855  reumodprminv  13055  nnnn0modprm0  13057  prmlem0  13243  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemsima  13311  ballotfilemrv  13315  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemf1  13361  ennnfonelemrn  13362  ctinfomlemom  13370  ctinfom  13371  ctiunctlemudc  13380  ctiunctlemf  13381  elrest  13653  ptex  13671  imasaddfnlemg  13688  divsfval  13702  xpscf  13721  grpidvalg  13746  grpidpropdg  13747  grpidd  13756  issgrpd  13780  sgrppropd  13781  ismndd  13803  mndpropd  13806  imasmnd2  13812  imasmnd  13813  ismhm  13821  issubm  13832  imasgrp2  13966  imasgrp  13967  issubg  14029  subginv  14037  isnsg  14058  eqg0el  14085  quselbasg  14086  isghm  14099  resghm2b  14118  conjnmzb  14136  conjnsg  14137  ghmpropd  14139  cntrval  14145  cntzval  14147  elcntz  14148  elcntzsn  14151  resscntz  14160  imasabl  14224  gzsumsplit0  14232  prdsbasmpt  14264  prdsbasmpt2  14272  pwselbasb  14290  mgpplusg  14306  mgpbas  14309  isrngd  14336  rngpropd  14338  imasrng  14339  qusrng  14341  rng1zrlem  14342  ringidval  14349  dfur2g  14350  srgidmlem  14366  issrgid  14369  ringcl  14401  isringid  14414  isringd  14430  imasring  14453  oppr0g  14471  oppr1g  14472  dvdsrvald  14484  isunitd  14497  unitinvcl  14514  unitinvinv  14515  unitlinv  14517  unitrinv  14518  unitnegcl  14521  dvdsrpropdg  14538  isrhm  14549  isrim0  14552  rhmmul  14555  islring  14583  opprlring  14588  issubrng  14591  opprsubrngg  14603  issubrg  14613  resrhm2b  14641  rhmpropd  14646  rrgval  14654  aprval  14675  aprap  14682  aprprop  14685  islmod  14711  lmodprop2d  14769  islssm  14778  islssmg  14779  islssmd  14780  lssats2  14835  ellspsn  14838  ixpsnbasval  14887  islidlm  14900  isridlrng  14903  rspssp  14915  rnglidlmmgm  14917  2idlval  14923  isridl  14925  2idlelb  14926  quscrng  14954  rspsn  14955  zrhval  15036  zrhrhmb  15041  znf1o  15070  asclfval  15105  assamulgscmlem2  15126  psrgrp  15167  mplelbascoe  15174  istopon  15205  eltg  15244  eltg2  15245  eltop  15261  eltop2  15262  eltop3  15263  iscld  15295  neiss2  15334  isnei  15336  lmfval  15385  cnfval  15386  iscn  15389  iscnp  15391  tgcn  15400  tgcnp  15401  lmbrf  15407  cnptopresti  15430  txbas  15450  eltx  15451  txdis  15469  txdis1cn  15470  hmeofvalg  15495  ishmeo  15496  ispsmet  15515  ismet  15536  isxmet  15537  elblps  15582  elbl  15583  elmopn  15638  neibl  15683  metrest  15698  txmetcnp  15710  txmetcn  15711  metcnpd  15712  elcncf  15765  ellimc3apf  15852  limcmpted  15855  cnlimcim  15863  cnlimc  15864  eldvap  15874  dvidsslem  15885  dviaddf  15897  dvimulf  15898  elply  15926  ply1termlem  15934  lgseisenlem3  16357  edgval  16467  edgiedgbg  16472  edgupgren  16548  upgredg  16551  uhgr2edg  16613  umgr2edg1  16616  usgredg2vlem1  16629  usgredg2vlem2  16630  ushgredgedg  16633  ushgredgedgloop  16635  subgruhgredgdm  16677  uhgrspansubgrlem  16683  vtxdgfval  16695  vtxedgfi  16696  vtxdgop  16699  vtxdg0v  16701  vtxdeqd  16703  vtxdfifiun  16704  1loopgrvd0fi  16713  1hevtxdg0fi  16714  1hevtxdg1en  16715  wksfval  16729  iswlk  16730  wlkm  16746  uspgr2wlkeq  16772  wlkreslem  16785  wlkres  16786  istrl  16792  clwwlkg  16800  isclwwlk  16801  clwwlkccatlem  16807  isclwwlkng  16813  clwwlkn0  16815  clwwlknnn  16819  clwwlkext2edg  16829  clwwlknonmpo  16835  clwwlknon  16836  clwwlk0on0  16838  iseupth  16854  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lembfi  16884  bj-sels  17106  pw1map  17191  wexmiddiffilem  17209  wexmiddifxylem  17211  nninfall  17218  nninfsellemeq  17223