Theorem eleq2d 2247

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  eleq12d  2248  eleqtrd  2256  neleqtrd  2275  neleqtrrd  2276  abeq2d  2290  nfceqdf  2318  drnfc1  2336  drnfc2  2337  sbcbid  3022  cbvcsbw  3063  cbvcsb  3064  sbcel1g  3078  csbeq2d  3084  csbie2g  3109  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  opeq1  3780  opeq2  3781  cbviun  3925  cbviin  3926  iinxsng  3962  iinxprg  3963  iunxsng  3964  iunxsngf  3966  cbvdisj  3992  disjnim  3996  disjiun  4000  mpteq12f  4085  axpweq  4173  rabxfrd  4471  onsucelsucexmid  4531  ordsucunielexmid  4532  0elsucexmid  4566  0nelelxp  4657  opeliunxp  4683  opeliunxp2  4769  iunxpf  4777  elrelimasn  4996  elimasng  4998  xpimasn  5079  ressn  5171  funfni  5318  fnbr  5320  fun11iun  5484  fvelrnb  5565  foelcdmi  5570  fvun1  5584  fvco2  5587  elfvmptrab1  5612  elfvmptrab  5613  elpreima  5637  dff3im  5663  resflem  5682  fmptco  5684  funfvima3  5752  foima2  5754  eluniimadm  5768  dff13  5771  f1eqcocnv  5794  isoini  5821  riotaeqdv  5834  mpoeq123dva  5938  cbvmpox  5955  ovelrn  6025  elovmpo  6074  fmpox  6203  disjxp1  6239  opeliunxp2f  6241  mpoxopn0yelv  6242  mpoxopovel  6244  rbropapd  6245  rntpos  6260  smoel  6303  smoiso  6305  smoel2  6306  tfrlem9  6322  tfrlemisucaccv  6328  tfrlemiubacc  6333  tfrlemi14d  6336  tfri2d  6339  tfr1onlemubacc  6349  tfr1onlemres  6352  tfrcllemubacc  6362  tfrcllemres  6365  rdgon  6389  freceq1  6395  freceq2  6396  frec0g  6400  frecabcl  6402  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecsuc  6410  nnsucelsuc  6494  nnsucuniel  6498  nnmordi  6519  ereldm  6580  iinerm  6609  elmapg  6663  elpmg  6666  elixpsn  6737  ixpsnf1o  6738  phplem4  6857  phplem3g  6858  phplem4on  6869  exmidpw  6910  fiintim  6930  fidcenumlemrks  6954  fidcenumlemrk  6955  elfi  6972  ordiso2  7036  ctssdccl  7112  nnnninfeq  7128  cc2lem  7267  cc2  7268  cc3  7269  archnqq  7418  ltdfpr  7507  genpelxp  7512  genpelvl  7513  genpelvu  7514  addcanprleml  7615  addcanprlemu  7616  cauappcvgprlem1  7660  suplocexprlemell  7714  suplocexprlemmu  7719  suplocexprlemru  7720  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  suplocexprlemlub  7725  cnm  7833  eluz1  9534  elixx1  9899  elioo2  9923  elfz1  10015  elfzp1  10074  fzpr  10079  fzsuc2  10081  fzrev3  10089  elfzp12  10101  fzm1  10102  fzoval  10150  elfzo  10151  fzodcel  10154  elfzom1b  10231  fzosplitsni  10237  zmodidfzo  10355  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  bcval  10731  bcpasc  10748  shftfn  10835  shftval  10836  seq3shft  10849  iser3shft  11356  sumeq1  11365  summodclem3  11390  summodclem2a  11391  isumss  11401  fsumsplit  11417  sumsplitdc  11442  fsum2dlemstep  11444  fisumcom2  11448  fsumparts  11480  explecnv  11515  fprodsplitdc  11606  fprodsplit  11607  fprod2dlemstep  11632  fprodcom2fi  11636  eftlub  11700  divalgmod  11934  nninfdcex  11956  algfx  12054  eucalgcvga  12060  reumodprminv  12255  nnnn0modprm0  12257  ennnfonelemex  12417  ennnfonelemhom  12418  ennnfonelemf1  12421  ennnfonelemrn  12422  ctinfomlemom  12430  ctinfom  12431  ctiunctlemudc  12440  ctiunctlemf  12441  elrest  12700  ptex  12718  imasaddfnlemg  12740  xpscf  12771  grpidvalg  12797  grpidpropdg  12798  grpidd  12807  ismndd  12843  mndpropd  12846  ismhm  12858  issubm  12868  issubg  13038  subginv  13046  isnsg  13067  dfur2g  13150  srgidmlem  13166  issrgid  13169  ringcl  13201  isringid  13213  isringd  13225  oppr0g  13256  oppr1g  13257  reldvdsrsrg  13266  dvdsrvald  13267  isunitd  13280  unitinvcl  13297  unitinvinv  13298  unitlinv  13300  unitrinv  13301  unitnegcl  13304  dvdsrpropdg  13321  islring  13338  issubrg  13347  aprval  13377  aprap  13381  islmod  13386  lmodprop2d  13443  islssm  13450  islssmd  13451  istopon  13552  eltg  13591  eltg2  13592  eltop  13608  eltop2  13609  eltop3  13610  iscld  13642  neiss2  13681  isnei  13683  lmfval  13731  cnfval  13733  iscn  13736  iscnp  13738  tgcn  13747  tgcnp  13748  lmbrf  13754  cnptopresti  13777  txbas  13797  eltx  13798  txdis  13816  txdis1cn  13817  hmeofvalg  13842  ishmeo  13843  ispsmet  13862  ismet  13883  isxmet  13884  elblps  13929  elbl  13930  elmopn  13985  neibl  14030  metrest  14045  txmetcnp  14057  txmetcn  14058  metcnpd  14059  elcncf  14099  ellimc3apf  14168  limcmpted  14171  cnlimcim  14179  cnlimc  14180  eldvap  14190  dviaddf  14208  dvimulf  14209  bj-sels  14705  nninfall  14797  nninfsellemeq  14802