Theorem eleq12d 2907

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)

Hypotheses

Ref	Expression
eleq12d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eleq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eleq12d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Proof of Theorem eleq12d

Step	Hyp	Ref	Expression
1		eleq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
2	1	eleq2d 2898	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq12d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2897	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 281	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893

This theorem is referenced by:  neleq12d  3127  cbvraldva2  3456  cbvrexdva2  3457  cbvrexdva2OLD  3458  cdeqel  3766  ru  3770  sbceqbid  3778  cbvrabcsfw  3923  cbvralcsf  3924  cbvreucsf  3926  cbvrabcsf  3927  sbcel12  4359  elvvuni  5622  elrnmpt1  5824  canth  7105  onnseq  7975  smoeq  7981  smores  7983  smores2  7985  iordsmo  7988  tz7.49  8075  nnaordr  8240  omsmolem  8274  fvixp  8460  cbvixp  8472  mptelixpg  8493  boxcutc  8499  ixpiunwdom  9049  elirr  9055  cantnflt  9129  oemapvali  9141  cantnflem1  9146  cantnf  9150  wemapwe  9154  cnfcom3lem  9160  infxpen  9434  dfac8alem  9449  dfac8clem  9452  ac5num  9456  acni2  9466  numacn  9469  acndom  9471  aceq3lem  9540  dfac5  9548  dfac9  9556  dfac13  9562  fin2i  9711  isfin2-2  9735  fin23lem27  9744  isfin3ds  9745  fin23lem17  9754  fin23lem39  9766  isf33lem  9782  isf34lem7  9795  isf34lem6  9796  fin1a2lem10  9825  fin1a2lem12  9827  hsmexlem4  9845  axcc2lem  9852  axcc3  9854  domtriomlem  9858  axdc2lem  9864  axdc3lem2  9867  axdc3lem3  9868  axdc3lem4  9869  axdc3  9870  axdc4lem  9871  axcclem  9873  ac6num  9895  ac6c4  9897  iundom2g  9956  fpwwe2  10059  pwfseqlem1  10074  pwfseqlem4a  10077  pwfseqlem4  10078  ltapi  10319  ltmpi  10320  eluzadd  12267  fzsubel  12937  elfzp1b  12978  axdc4uzlem  13345  wrd2ind  14079  smuval  15824  prdsbasprj  16739  xpsfrnel  16829  ismri2dad  16902  mreexd  16907  mreacs  16923  iscat  16937  iscatd  16938  iscatd2  16946  catcocl  16950  catpropd  16973  brssc  17078  issubc  17099  subcidcl  17108  subccocl  17109  isfunc  17128  isfuncd  17129  cofucl  17152  funcres2b  17161  fuciso  17239  yonedalem3  17524  yonffthlem  17526  ismgm  17847  issstrmgm  17857  ismndd  17927  eqgfval  18322  efgsdm  18850  efgsdmi  18852  efgsrel  18854  efgsp1  18857  efgsres  18858  dprdfcl  19129  ablfaclem3  19203  isdrngd  19521  issrng  19615  issrngd  19626  islmodd  19634  islbs  19842  lbsind  19846  lbspropd  19865  islbs2  19920  lbsextlem4  19927  lbsextg  19928  zndvds  20690  isphl  20766  isphld  20792  phlpropd  20793  frlmlbs  20935  islindf  20950  islinds2  20951  lindfind  20954  lindsind  20955  lindsind2  20957  lindfrn  20959  lindfmm  20965  lsslindf  20968  mat1dimmul  21079  istps  21536  tpspropd  21540  eltpsg  21545  islp  21742  1stcelcls  22063  kgeni  22139  kgencn2  22159  ptpjpre1  22173  elptr2  22176  ptbasin  22179  ptbasfi  22183  ptpjcn  22213  ptpjopn  22214  ptcld  22215  ptcldmpt  22216  ptclsg  22217  ptcnp  22224  qtopval  22297  ptcmplem2  22655  ptcmplem3  22656  ptcmplem4  22657  istmd  22676  istgp  22679  tmdgsum  22697  istlm  22787  isusp  22864  prdsdsf  22971  prdsxmet  22973  isms  23053  mspropd  23078  setsxms  23083  setsms  23084  tmsxms  23090  tmsms  23091  isnrg  23263  tngnrg  23277  bcthlem2  23922  bcthlem3  23923  bcthlem4  23924  bcthlem5  23925  iscms  23942  cmspropd  23946  cmssmscld  23947  cmsss  23948  shft2rab  24103  ovolicc2lem3  24114  ovolicc2lem4  24115  ovolicc2lem5  24116  vitalilem2  24204  vitalilem3  24205  vitali  24208  limcfval  24464  limcmpt2  24476  limcres  24478  cnplimc  24479  cnlimci  24481  elcpn  24525  uc1pval  24727  ig1pcl  24763  jensen  25560  axtgcont  26249  tglngval  26331  ishlg  26382  mirbtwnb  26452  trgcopy  26584  trgcopyeu  26586  acopyeu  26614  isinagd  26619  tgasa1  26638  wlkp1lem3  27451  umgrwwlks2on  27730  clwwlknon1  27870  clwwlknonclwlknonf1o  28135  imsmet  28462  smcn  28469  iscbn  28635  sbceqbidf  30244  fnpreimac  30410  isslmd  30825  0nellinds  30930  lindssn  30934  lindfpropd  30937  lbslsat  31009  lindsunlem  31015  brfldext  31032  submateq  31069  lmatcl  31076  ispcmp  31116  zhmnrg  31203  ismntoplly  31261  inelpisys  31408  sigapildsys  31416  fiunelcarsg  31569  eulerpartlemgvv  31629  eulerpart  31635  ptpconn  32475  cvmscbv  32500  cvmshmeo  32513  cvmsss2  32516  cvmliftlem7  32533  cvmliftlem10  32536  cvmlift2lem11  32555  cvmlift2lem12  32556  satffunlem1lem1  32644  satffunlem2lem1  32646  sategoelfvb  32661  prv1n  32673  elmpps  32815  currysetlem  34251  currysetlem1  34253  bj-ismoore  34391  csbfinxpg  34663  pibt2  34692  lindsadd  34879  lindsenlbs  34881  ptrest  34885  upixp  34998  sdclem1  35012  sstotbnd2  35046  prdsbnd2  35067  isprrngo  35322  isopos  36310  isatl  36429  isnacs3  39300  nacsfix  39302  mzpclall  39317  dnnumch1  39637  dnwech  39641  aomclem3  39649  aomclem8  39654  dfac11  39655  islmodfg  39662  rfovcnvf1od  40343  ismnu  40590  sblpnf  40635  rusbcALT  40764  choicefi  41456  climsuselem1  41881  climsuse  41882  cncfuni  42162  dvnprodlem1  42224  stoweidlem31  42310  stoweidlem59  42338  fourierdlem46  42431  fourierdlem62  42447  fourierdlem72  42457  fourierdlem79  42464  fourierdlem88  42473  fourierdlem89  42474  fourierdlem90  42475  fourierdlem91  42476  fourierdlem112  42497  qndenserrnbllem  42573  ioorrnopnlem  42583  ioorrnopn  42584  ioorrnopnxr  42586  issal  42593  subsaliuncllem  42634  subsaliuncl  42635  subsalsal  42636  sge0tsms  42656  sge0iunmpt  42694  sge0seq  42722  ovnsubaddlem1  42846  ovnsubaddlem2  42847  hoidmvlelem3  42873  hoidmvlelem4  42874  rrnmbl  42890  hoiqssbllem3  42900  hspmbl  42905  hoimbl  42907  issmflem  42998  issmfd  43006  issmfdf  43008  smfpimltmpt  43017  issmfled  43028  smfpimltxrmpt  43029  smfmbfcex  43030  issmfgtd  43031  smflimlem1  43041  smflimlem2  43042  smflimlem3  43043  smflimlem6  43046  smfpimgtmpt  43051  smfpimgtxrmpt  43054  smfres  43059  smfco  43071  smfpimcclem  43075  smfpimcc  43076  dfateq12d  43319  ismgmd  44037  iscllaw  44090  islininds  44495