Theorem eleq2d 2209

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  eleq12d  2210  eleqtrd  2218  neleqtrd  2237  neleqtrrd  2238  abeq2d  2252  nfceqdf  2280  drnfc1  2298  drnfc2  2299  sbcbid  2966  cbvcsbw  3007  cbvcsb  3008  sbcel1g  3021  csbeq2d  3027  csbie2g  3050  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  opeq1  3705  opeq2  3706  cbviun  3850  cbviin  3851  iinxsng  3886  iinxprg  3887  iunxsng  3888  iunxsngf  3890  cbvdisj  3916  disjnim  3920  disjiun  3924  mpteq12f  4008  axpweq  4095  rabxfrd  4390  onsucelsucexmid  4445  ordsucunielexmid  4446  0elsucexmid  4480  0nelelxp  4568  opeliunxp  4594  opeliunxp2  4679  iunxpf  4687  elreimasng  4905  elimasng  4907  xpimasn  4987  ressn  5079  funfni  5223  fnbr  5225  fun11iun  5388  fvelrnb  5469  fvun1  5487  fvco2  5490  elfvmptrab1  5515  elfvmptrab  5516  elpreima  5539  dff3im  5565  resflem  5584  fmptco  5586  funfvima3  5651  foima2  5653  eluniimadm  5666  dff13  5669  f1eqcocnv  5692  isoini  5719  riotaeqdv  5731  mpoeq123dva  5832  cbvmpox  5849  ovelrn  5919  elovmpo  5971  fmpox  6098  disjxp1  6133  opeliunxp2f  6135  mpoxopn0yelv  6136  mpoxopovel  6138  rbropapd  6139  rntpos  6154  smoel  6197  smoiso  6199  smoel2  6200  tfrlem9  6216  tfrlemisucaccv  6222  tfrlemiubacc  6227  tfrlemi14d  6230  tfri2d  6233  tfr1onlemubacc  6243  tfr1onlemres  6246  tfrcllemubacc  6256  tfrcllemres  6259  rdgon  6283  freceq1  6289  freceq2  6290  frec0g  6294  frecabcl  6296  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecsuc  6304  nnsucelsuc  6387  nnsucuniel  6391  nnmordi  6412  ereldm  6472  iinerm  6501  elmapg  6555  elpmg  6558  elixpsn  6629  ixpsnf1o  6630  phplem4  6749  phplem3g  6750  phplem4on  6761  exmidpw  6802  fiintim  6817  fidcenumlemrks  6841  fidcenumlemrk  6842  elfi  6859  ordiso2  6920  ctssdccl  6996  archnqq  7225  ltdfpr  7314  genpelxp  7319  genpelvl  7320  genpelvu  7321  addcanprleml  7422  addcanprlemu  7423  cauappcvgprlem1  7467  suplocexprlemell  7521  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  suplocexprlemlub  7532  cnm  7640  eluz1  9330  elixx1  9680  elioo2  9704  elfz1  9795  elfzp1  9852  fzpr  9857  fzsuc2  9859  fzrev3  9867  elfzp12  9879  fzm1  9880  fzoval  9925  elfzo  9926  fzodcel  9929  elfzom1b  10006  fzosplitsni  10012  zmodidfzo  10126  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  bcval  10495  bcpasc  10512  shftfn  10596  shftval  10597  seq3shft  10610  iser3shft  11115  sumeq1  11124  summodclem3  11149  summodclem2a  11150  isumss  11160  fsumsplit  11176  sumsplitdc  11201  fsum2dlemstep  11203  fisumcom2  11207  fsumparts  11239  explecnv  11274  eftlub  11396  divalgmod  11624  algfx  11733  eucalgcvga  11739  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemf1  11931  ennnfonelemrn  11932  ctinfomlemom  11940  ctinfom  11941  ctiunctlemudc  11950  ctiunctlemf  11951  elrest  12127  istopon  12180  eltg  12221  eltg2  12222  eltop  12238  eltop2  12239  eltop3  12240  iscld  12272  neiss2  12311  isnei  12313  lmfval  12361  cnfval  12363  iscn  12366  iscnp  12368  tgcn  12377  tgcnp  12378  lmbrf  12384  cnptopresti  12407  txbas  12427  eltx  12428  txdis  12446  txdis1cn  12447  hmeofvalg  12472  ishmeo  12473  ispsmet  12492  ismet  12513  isxmet  12514  elblps  12559  elbl  12560  elmopn  12615  neibl  12660  metrest  12675  txmetcnp  12687  txmetcn  12688  metcnpd  12689  elcncf  12729  ellimc3apf  12798  limcmpted  12801  cnlimcim  12809  cnlimc  12810  eldvap  12820  dviaddf  12838  dvimulf  12839  bj-sels  13112  nninfalllemn  13202  nninfall  13204  nninfsellemeq  13210