Theorem eleq2d 2240

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ∈ wcel 2141

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eleq12d  2241  eleqtrd  2249  neleqtrd  2268  neleqtrrd  2269  abeq2d  2283  nfceqdf  2311  drnfc1  2329  drnfc2  2330  sbcbid  3012  cbvcsbw  3053  cbvcsb  3054  sbcel1g  3068  csbeq2d  3074  csbie2g  3099  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  opeq1  3763  opeq2  3764  cbviun  3908  cbviin  3909  iinxsng  3944  iinxprg  3945  iunxsng  3946  iunxsngf  3948  cbvdisj  3974  disjnim  3978  disjiun  3982  mpteq12f  4067  axpweq  4155  rabxfrd  4452  onsucelsucexmid  4512  ordsucunielexmid  4513  0elsucexmid  4547  0nelelxp  4638  opeliunxp  4664  opeliunxp2  4749  iunxpf  4757  elreimasng  4975  elimasng  4977  xpimasn  5057  ressn  5149  funfni  5296  fnbr  5298  fun11iun  5461  fvelrnb  5542  fvun1  5560  fvco2  5563  elfvmptrab1  5588  elfvmptrab  5589  elpreima  5613  dff3im  5639  resflem  5658  fmptco  5660  funfvima3  5727  foima2  5729  eluniimadm  5742  dff13  5745  f1eqcocnv  5768  isoini  5795  riotaeqdv  5808  mpoeq123dva  5912  cbvmpox  5929  ovelrn  5999  elovmpo  6048  fmpox  6177  disjxp1  6213  opeliunxp2f  6215  mpoxopn0yelv  6216  mpoxopovel  6218  rbropapd  6219  rntpos  6234  smoel  6277  smoiso  6279  smoel2  6280  tfrlem9  6296  tfrlemisucaccv  6302  tfrlemiubacc  6307  tfrlemi14d  6310  tfri2d  6313  tfr1onlemubacc  6323  tfr1onlemres  6326  tfrcllemubacc  6336  tfrcllemres  6339  rdgon  6363  freceq1  6369  freceq2  6370  frec0g  6374  frecabcl  6376  freccllem  6379  frecfcllem  6381  frecsuclem  6383  frecsuc  6384  nnsucelsuc  6468  nnsucuniel  6472  nnmordi  6493  ereldm  6554  iinerm  6583  elmapg  6637  elpmg  6640  elixpsn  6711  ixpsnf1o  6712  phplem4  6831  phplem3g  6832  phplem4on  6843  exmidpw  6884  fiintim  6904  fidcenumlemrks  6928  fidcenumlemrk  6929  elfi  6946  ordiso2  7010  ctssdccl  7086  nnnninfeq  7102  cc2lem  7221  cc2  7222  cc3  7223  archnqq  7372  ltdfpr  7461  genpelxp  7466  genpelvl  7467  genpelvu  7468  addcanprleml  7569  addcanprlemu  7570  cauappcvgprlem1  7614  suplocexprlemell  7668  suplocexprlemmu  7673  suplocexprlemru  7674  suplocexprlemdisj  7675  suplocexprlemloc  7676  suplocexprlemub  7678  suplocexprlemlub  7679  cnm  7787  eluz1  9484  elixx1  9847  elioo2  9871  elfz1  9963  elfzp1  10021  fzpr  10026  fzsuc2  10028  fzrev3  10036  elfzp12  10048  fzm1  10049  fzoval  10097  elfzo  10098  fzodcel  10101  elfzom1b  10178  fzosplitsni  10184  zmodidfzo  10302  frecuzrdgtcl  10361  frecuzrdgfunlem  10368  bcval  10676  bcpasc  10693  shftfn  10781  shftval  10782  seq3shft  10795  iser3shft  11302  sumeq1  11311  summodclem3  11336  summodclem2a  11337  isumss  11347  fsumsplit  11363  sumsplitdc  11388  fsum2dlemstep  11390  fisumcom2  11394  fsumparts  11426  explecnv  11461  fprodsplitdc  11552  fprodsplit  11553  fprod2dlemstep  11578  fprodcom2fi  11582  eftlub  11646  divalgmod  11879  nninfdcex  11901  algfx  11999  eucalgcvga  12005  reumodprminv  12200  nnnn0modprm0  12202  ennnfonelemex  12362  ennnfonelemhom  12363  ennnfonelemf1  12366  ennnfonelemrn  12367  ctinfomlemom  12375  ctinfom  12376  ctiunctlemudc  12385  ctiunctlemf  12386  elrest  12579  grpidvalg  12620  grpidpropdg  12621  grpidd  12630  ismndd  12666  mndpropd  12669  ismhm  12678  issubm  12688  istopon  12770  eltg  12811  eltg2  12812  eltop  12828  eltop2  12829  eltop3  12830  iscld  12862  neiss2  12901  isnei  12903  lmfval  12951  cnfval  12953  iscn  12956  iscnp  12958  tgcn  12967  tgcnp  12968  lmbrf  12974  cnptopresti  12997  txbas  13017  eltx  13018  txdis  13036  txdis1cn  13037  hmeofvalg  13062  ishmeo  13063  ispsmet  13082  ismet  13103  isxmet  13104  elblps  13149  elbl  13150  elmopn  13205  neibl  13250  metrest  13265  txmetcnp  13277  txmetcn  13278  metcnpd  13279  elcncf  13319  ellimc3apf  13388  limcmpted  13391  cnlimcim  13399  cnlimc  13400  eldvap  13410  dviaddf  13428  dvimulf  13429  bj-sels  13914  nninfall  14007  nninfsellemeq  14012