Theorem eleq2d 2276

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  eleq12d  2277  eleqtrd  2285  neleqtrd  2304  neleqtrrd  2305  abeq2d  2319  nfceqdf  2348  drnfc1  2366  drnfc2  2367  sbcbid  3060  cbvcsbw  3101  cbvcsb  3102  sbcel1g  3116  csbeq2d  3122  csbie2g  3148  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  opeq1  3825  opeq2  3826  cbviun  3970  cbviin  3971  iinxsng  4007  iinxprg  4008  iunxsng  4009  iunxsngf  4011  cbvdisj  4037  disjnim  4041  disjiun  4046  mpteq12f  4132  axpweq  4223  rabxfrd  4524  onsucelsucexmid  4586  ordsucunielexmid  4587  0elsucexmid  4621  0nelelxp  4712  opeliunxp  4738  opeliunxp2  4826  iunxpf  4834  elrelimasn  5057  elimasng  5059  xpimasn  5140  ressn  5232  funfni  5385  fnbr  5387  fun11iun  5555  fvelrnb  5639  foelcdmi  5644  fvun1  5658  fvco2  5661  elfvmptrab1  5687  elfvmptrab  5688  elpreima  5712  dff3im  5738  resflem  5757  fmptco  5759  funfvima3  5831  foima2  5833  eluniimadm  5847  dff13  5850  f1eqcocnv  5873  isoini  5900  riotaeqdv  5913  mpoeq123dva  6019  cbvmpox  6036  ovelrn  6108  elovmpod  6157  elovmpo  6158  elovmporab  6159  elovmporab1w  6160  fmpox  6299  disjxp1  6335  opeliunxp2f  6337  mpoxopn0yelv  6338  mpoxopovel  6340  rbropapd  6341  rntpos  6356  smoel  6399  smoiso  6401  smoel2  6402  tfrlem9  6418  tfrlemisucaccv  6424  tfrlemiubacc  6429  tfrlemi14d  6432  tfri2d  6435  tfr1onlemubacc  6445  tfr1onlemres  6448  tfrcllemubacc  6458  tfrcllemres  6461  rdgon  6485  freceq1  6491  freceq2  6492  frec0g  6496  frecabcl  6498  freccllem  6501  frecfcllem  6503  frecsuclem  6505  frecsuc  6506  nnsucelsuc  6590  nnsucuniel  6594  nnmordi  6615  ereldm  6678  iinerm  6707  elmapg  6761  elpmg  6764  elixpsn  6835  ixpsnf1o  6836  pw2f1odclem  6946  phplem4  6967  phplem3g  6968  phplem4on  6979  exmidpw  7020  fiintim  7043  fidcenumlemrks  7070  fidcenumlemrk  7071  elfi  7088  ordiso2  7152  ctssdccl  7228  nnnninfeq  7245  cc2lem  7398  cc2  7399  cc3  7400  archnqq  7550  ltdfpr  7639  genpelxp  7644  genpelvl  7645  genpelvu  7646  addcanprleml  7747  addcanprlemu  7748  cauappcvgprlem1  7792  suplocexprlemell  7846  suplocexprlemmu  7851  suplocexprlemru  7852  suplocexprlemdisj  7853  suplocexprlemloc  7854  suplocexprlemub  7856  suplocexprlemlub  7857  cnm  7965  eluz1  9672  elixx1  10039  elioo2  10063  elfz1  10155  elfzp1  10214  fzpr  10219  fzsuc2  10221  fzrev3  10229  elfzp12  10241  fzm1  10242  fzoval  10290  elfzo  10291  fzodcel  10295  elfzom1b  10380  fzosplitsni  10386  nninfdcex  10402  zmodidfzo  10520  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  seqf1og  10688  bcval  10916  bcpasc  10933  fundm2domnop0  11012  wrdmap  11047  elovmpowrd  11057  ccatfvalfi  11071  elfzelfzccat  11079  ccatlid  11085  ccatass  11087  ccatrn  11088  swrdfv2  11139  ccatswrd  11146  swrdccat2  11147  pfxfv  11160  pfxeq  11172  ccatpfx  11177  swrdswrd  11181  swrdpfx  11183  pfxpfx  11184  cats1un  11197  shftfn  11210  shftval  11211  seq3shft  11224  iser3shft  11732  sumeq1  11741  summodclem3  11766  summodclem2a  11767  isumss  11777  fsumsplit  11793  sumsplitdc  11818  fsum2dlemstep  11820  fisumcom2  11824  fsumparts  11856  explecnv  11891  fprodsplitdc  11982  fprodsplit  11983  fprod2dlemstep  12008  fprodcom2fi  12012  eftlub  12076  divalgmod  12313  bitsval  12329  bitsp1e  12338  bitsp1o  12339  algfx  12449  eucalgcvga  12455  reumodprminv  12651  nnnn0modprm0  12653  ennnfonelemex  12860  ennnfonelemhom  12861  ennnfonelemf1  12864  ennnfonelemrn  12865  ctinfomlemom  12873  ctinfom  12874  ctiunctlemudc  12883  ctiunctlemf  12884  elrest  13153  ptex  13171  prdsbasmpt  13187  prdsbasmpt2  13195  pwselbasb  13200  imasaddfnlemg  13221  divsfval  13235  xpscf  13254  grpidvalg  13280  grpidpropdg  13281  grpidd  13290  issgrpd  13319  sgrppropd  13320  ismndd  13344  mndpropd  13347  imasmnd2  13359  imasmnd  13360  ismhm  13368  issubm  13379  imasgrp2  13521  imasgrp  13522  issubg  13584  subginv  13592  isnsg  13613  eqg0el  13640  quselbasg  13641  isghm  13654  resghm2b  13673  conjnmzb  13691  conjnsg  13692  ghmpropd  13694  imasabl  13747  isrngd  13790  rngpropd  13792  imasrng  13793  qusrng  13795  dfur2g  13799  srgidmlem  13815  issrgid  13818  ringcl  13850  isringid  13862  isringd  13878  imasring  13901  oppr0g  13918  oppr1g  13919  reldvdsrsrg  13929  dvdsrvald  13930  isunitd  13943  unitinvcl  13960  unitinvinv  13961  unitlinv  13963  unitrinv  13964  unitnegcl  13967  dvdsrpropdg  13984  isrhm  13995  isrim0  13998  rhmmul  14001  islring  14029  issubrng  14036  opprsubrngg  14048  issubrg  14058  resrhm2b  14086  rhmpropd  14091  rrgval  14099  aprval  14119  aprap  14123  islmod  14128  lmodprop2d  14185  islssm  14194  islssmg  14195  islssmd  14196  lssats2  14251  ellspsn  14254  ixpsnbasval  14303  islidlm  14316  isridlrng  14319  rspssp  14331  rnglidlmmgm  14333  2idlval  14339  isridl  14341  2idlelb  14342  quscrng  14370  rspsn  14371  zrhval  14454  zrhrhmb  14459  znf1o  14488  psrgrp  14522  mplelbascoe  14529  istopon  14560  eltg  14599  eltg2  14600  eltop  14616  eltop2  14617  eltop3  14618  iscld  14650  neiss2  14689  isnei  14691  lmfval  14739  cnfval  14741  iscn  14744  iscnp  14746  tgcn  14755  tgcnp  14756  lmbrf  14762  cnptopresti  14785  txbas  14805  eltx  14806  txdis  14824  txdis1cn  14825  hmeofvalg  14850  ishmeo  14851  ispsmet  14870  ismet  14891  isxmet  14892  elblps  14937  elbl  14938  elmopn  14993  neibl  15038  metrest  15053  txmetcnp  15065  txmetcn  15066  metcnpd  15067  elcncf  15120  ellimc3apf  15207  limcmpted  15210  cnlimcim  15218  cnlimc  15219  eldvap  15229  dvidsslem  15240  dviaddf  15252  dvimulf  15253  elply  15281  ply1termlem  15289  lgseisenlem3  15624  edgiedgbg  15736  bj-sels  15988  2omap  16071  pw1map  16073  nninfall  16087  nninfsellemeq  16092