Theorem eleq2d 2235

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 2229	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1343   ∈ wcel 2136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-clel 2161

This theorem is referenced by:  eleq12d  2236  eleqtrd  2244  neleqtrd  2263  neleqtrrd  2264  abeq2d  2278  nfceqdf  2306  drnfc1  2324  drnfc2  2325  sbcbid  3007  cbvcsbw  3048  cbvcsb  3049  sbcel1g  3063  csbeq2d  3069  csbie2g  3094  cbvralcsf  3106  cbvrexcsf  3107  cbvreucsf  3108  cbvrabcsf  3109  opeq1  3757  opeq2  3758  cbviun  3902  cbviin  3903  iinxsng  3938  iinxprg  3939  iunxsng  3940  iunxsngf  3942  cbvdisj  3968  disjnim  3972  disjiun  3976  mpteq12f  4061  axpweq  4149  rabxfrd  4446  onsucelsucexmid  4506  ordsucunielexmid  4507  0elsucexmid  4541  0nelelxp  4632  opeliunxp  4658  opeliunxp2  4743  iunxpf  4751  elreimasng  4969  elimasng  4971  xpimasn  5051  ressn  5143  funfni  5287  fnbr  5289  fun11iun  5452  fvelrnb  5533  fvun1  5551  fvco2  5554  elfvmptrab1  5579  elfvmptrab  5580  elpreima  5603  dff3im  5629  resflem  5648  fmptco  5650  funfvima3  5717  foima2  5719  eluniimadm  5732  dff13  5735  f1eqcocnv  5758  isoini  5785  riotaeqdv  5798  mpoeq123dva  5899  cbvmpox  5916  ovelrn  5986  elovmpo  6038  fmpox  6165  disjxp1  6200  opeliunxp2f  6202  mpoxopn0yelv  6203  mpoxopovel  6205  rbropapd  6206  rntpos  6221  smoel  6264  smoiso  6266  smoel2  6267  tfrlem9  6283  tfrlemisucaccv  6289  tfrlemiubacc  6294  tfrlemi14d  6297  tfri2d  6300  tfr1onlemubacc  6310  tfr1onlemres  6313  tfrcllemubacc  6323  tfrcllemres  6326  rdgon  6350  freceq1  6356  freceq2  6357  frec0g  6361  frecabcl  6363  freccllem  6366  frecfcllem  6368  frecsuclem  6370  frecsuc  6371  nnsucelsuc  6455  nnsucuniel  6459  nnmordi  6480  ereldm  6540  iinerm  6569  elmapg  6623  elpmg  6626  elixpsn  6697  ixpsnf1o  6698  phplem4  6817  phplem3g  6818  phplem4on  6829  exmidpw  6870  fiintim  6890  fidcenumlemrks  6914  fidcenumlemrk  6915  elfi  6932  ordiso2  6996  ctssdccl  7072  nnnninfeq  7088  cc2lem  7203  cc2  7204  cc3  7205  archnqq  7354  ltdfpr  7443  genpelxp  7448  genpelvl  7449  genpelvu  7450  addcanprleml  7551  addcanprlemu  7552  cauappcvgprlem1  7596  suplocexprlemell  7650  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  suplocexprlemlub  7661  cnm  7769  eluz1  9466  elixx1  9829  elioo2  9853  elfz1  9945  elfzp1  10003  fzpr  10008  fzsuc2  10010  fzrev3  10018  elfzp12  10030  fzm1  10031  fzoval  10079  elfzo  10080  fzodcel  10083  elfzom1b  10160  fzosplitsni  10166  zmodidfzo  10284  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  bcval  10658  bcpasc  10675  shftfn  10762  shftval  10763  seq3shft  10776  iser3shft  11283  sumeq1  11292  summodclem3  11317  summodclem2a  11318  isumss  11328  fsumsplit  11344  sumsplitdc  11369  fsum2dlemstep  11371  fisumcom2  11375  fsumparts  11407  explecnv  11442  fprodsplitdc  11533  fprodsplit  11534  fprod2dlemstep  11559  fprodcom2fi  11563  eftlub  11627  divalgmod  11860  nninfdcex  11882  algfx  11980  eucalgcvga  11986  reumodprminv  12181  nnnn0modprm0  12183  ennnfonelemex  12343  ennnfonelemhom  12344  ennnfonelemf1  12347  ennnfonelemrn  12348  ctinfomlemom  12356  ctinfom  12357  ctiunctlemudc  12366  ctiunctlemf  12367  elrest  12558  istopon  12611  eltg  12652  eltg2  12653  eltop  12669  eltop2  12670  eltop3  12671  iscld  12703  neiss2  12742  isnei  12744  lmfval  12792  cnfval  12794  iscn  12797  iscnp  12799  tgcn  12808  tgcnp  12809  lmbrf  12815  cnptopresti  12838  txbas  12858  eltx  12859  txdis  12877  txdis1cn  12878  hmeofvalg  12903  ishmeo  12904  ispsmet  12923  ismet  12944  isxmet  12945  elblps  12990  elbl  12991  elmopn  13046  neibl  13091  metrest  13106  txmetcnp  13118  txmetcn  13119  metcnpd  13120  elcncf  13160  ellimc3apf  13229  limcmpted  13232  cnlimcim  13240  cnlimc  13241  eldvap  13251  dviaddf  13269  dvimulf  13270  bj-sels  13756  nninfall  13849  nninfsellemeq  13854