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  3020  cbvcsbw  3061  cbvcsb  3062  sbcel1g  3076  csbeq2d  3082  csbie2g  3107  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  opeq1  3778  opeq2  3779  cbviun  3923  cbviin  3924  iinxsng  3960  iinxprg  3961  iunxsng  3962  iunxsngf  3964  cbvdisj  3990  disjnim  3994  disjiun  3998  mpteq12f  4083  axpweq  4171  rabxfrd  4469  onsucelsucexmid  4529  ordsucunielexmid  4530  0elsucexmid  4564  0nelelxp  4655  opeliunxp  4681  opeliunxp2  4767  iunxpf  4775  elrelimasn  4994  elimasng  4996  xpimasn  5077  ressn  5169  funfni  5316  fnbr  5318  fun11iun  5482  fvelrnb  5563  foelcdmi  5568  fvun1  5582  fvco2  5585  elfvmptrab1  5610  elfvmptrab  5611  elpreima  5635  dff3im  5661  resflem  5680  fmptco  5682  funfvima3  5750  foima2  5752  eluniimadm  5765  dff13  5768  f1eqcocnv  5791  isoini  5818  riotaeqdv  5831  mpoeq123dva  5935  cbvmpox  5952  ovelrn  6022  elovmpo  6071  fmpox  6200  disjxp1  6236  opeliunxp2f  6238  mpoxopn0yelv  6239  mpoxopovel  6241  rbropapd  6242  rntpos  6257  smoel  6300  smoiso  6302  smoel2  6303  tfrlem9  6319  tfrlemisucaccv  6325  tfrlemiubacc  6330  tfrlemi14d  6333  tfri2d  6336  tfr1onlemubacc  6346  tfr1onlemres  6349  tfrcllemubacc  6359  tfrcllemres  6362  rdgon  6386  freceq1  6392  freceq2  6393  frec0g  6397  frecabcl  6399  freccllem  6402  frecfcllem  6404  frecsuclem  6406  frecsuc  6407  nnsucelsuc  6491  nnsucuniel  6495  nnmordi  6516  ereldm  6577  iinerm  6606  elmapg  6660  elpmg  6663  elixpsn  6734  ixpsnf1o  6735  phplem4  6854  phplem3g  6855  phplem4on  6866  exmidpw  6907  fiintim  6927  fidcenumlemrks  6951  fidcenumlemrk  6952  elfi  6969  ordiso2  7033  ctssdccl  7109  nnnninfeq  7125  cc2lem  7264  cc2  7265  cc3  7266  archnqq  7415  ltdfpr  7504  genpelxp  7509  genpelvl  7510  genpelvu  7511  addcanprleml  7612  addcanprlemu  7613  cauappcvgprlem1  7657  suplocexprlemell  7711  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  suplocexprlemlub  7722  cnm  7830  eluz1  9531  elixx1  9896  elioo2  9920  elfz1  10012  elfzp1  10071  fzpr  10076  fzsuc2  10078  fzrev3  10086  elfzp12  10098  fzm1  10099  fzoval  10147  elfzo  10148  fzodcel  10151  elfzom1b  10228  fzosplitsni  10234  zmodidfzo  10352  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  bcval  10728  bcpasc  10745  shftfn  10832  shftval  10833  seq3shft  10846  iser3shft  11353  sumeq1  11362  summodclem3  11387  summodclem2a  11388  isumss  11398  fsumsplit  11414  sumsplitdc  11439  fsum2dlemstep  11441  fisumcom2  11445  fsumparts  11477  explecnv  11512  fprodsplitdc  11603  fprodsplit  11604  fprod2dlemstep  11629  fprodcom2fi  11633  eftlub  11697  divalgmod  11931  nninfdcex  11953  algfx  12051  eucalgcvga  12057  reumodprminv  12252  nnnn0modprm0  12254  ennnfonelemex  12414  ennnfonelemhom  12415  ennnfonelemf1  12418  ennnfonelemrn  12419  ctinfomlemom  12427  ctinfom  12428  ctiunctlemudc  12437  ctiunctlemf  12438  elrest  12694  ptex  12712  imasaddfnlemg  12734  xpscf  12765  grpidvalg  12791  grpidpropdg  12792  grpidd  12801  ismndd  12837  mndpropd  12840  ismhm  12852  issubm  12862  issubg  13031  subginv  13039  isnsg  13060  dfur2g  13143  srgidmlem  13159  issrgid  13162  ringcl  13194  isringid  13206  isringd  13218  oppr0g  13249  oppr1g  13250  reldvdsrsrg  13259  dvdsrvald  13260  isunitd  13273  unitinvcl  13290  unitinvinv  13291  unitlinv  13293  unitrinv  13294  unitnegcl  13297  dvdsrpropdg  13314  islring  13331  issubrg  13340  aprval  13370  aprap  13374  islmod  13379  istopon  13483  eltg  13522  eltg2  13523  eltop  13539  eltop2  13540  eltop3  13541  iscld  13573  neiss2  13612  isnei  13614  lmfval  13662  cnfval  13664  iscn  13667  iscnp  13669  tgcn  13678  tgcnp  13679  lmbrf  13685  cnptopresti  13708  txbas  13728  eltx  13729  txdis  13747  txdis1cn  13748  hmeofvalg  13773  ishmeo  13774  ispsmet  13793  ismet  13814  isxmet  13815  elblps  13860  elbl  13861  elmopn  13916  neibl  13961  metrest  13976  txmetcnp  13988  txmetcn  13989  metcnpd  13990  elcncf  14030  ellimc3apf  14099  limcmpted  14102  cnlimcim  14110  cnlimc  14111  eldvap  14121  dviaddf  14139  dvimulf  14140  bj-sels  14636  nninfall  14728  nninfsellemeq  14733