Theorem eleq12d 2858

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 2850	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq12d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2849	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 282	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  neleq12d  3070  cbvraldva2  3340  cdeqel  3737  sbceqbid  3749  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4372  elvvuni  5736  elrnmpt1  5954  canth  7405  onnseq  8390  smoeq  8396  smores  8398  smores2  8400  iordsmo  8403  tz7.49  8493  nnaordr  8667  omsmolem  8704  naddel2  8736  fvixp  8968  cbvixp  8980  cbvixpv  8981  mptelixpg  9001  boxcutc  9007  ixpiunwdom  9621  elirr  9631  cantnflt  9710  oemapvali  9722  cantnflem1  9727  cantnf  9731  wemapwe  9735  cnfcom3lem  9741  ttrcltr  9754  rnttrcl  9760  infxpen  10132  dfac8alem  10147  dfac8clem  10150  ac5num  10154  acni2  10164  numacn  10167  acndom  10169  aceq3lem  10238  dfac5  10246  dfac9  10254  dfac13  10260  fin2i  10412  isfin2-2  10436  fin23lem27  10445  isfin3ds  10446  fin23lem17  10455  fin23lem39  10467  isf33lem  10483  isf34lem7  10496  isf34lem6  10497  fin1a2lem10  10526  fin1a2lem12  10528  hsmexlem4  10546  axcc2lem  10553  axcc3  10555  domtriomlem  10559  axdc2lem  10565  axdc3lem2  10568  axdc3lem3  10569  axdc3lem4  10570  axdc3  10571  axdc4lem  10572  axcclem  10574  ac6num  10596  ac6c4  10598  iundom2g  10663  fpwwe2  10767  pwfseqlem1  10782  pwfseqlem4a  10785  pwfseqlem4  10786  ltapi  11027  ltmpi  11028  fzsubel  13734  elfzp1b  13775  axdc4uzlem  14166  wrd2ind  14914  smuval  16695  prdsbasprj  17693  xpsfrnel  17784  ismri2dad  17861  mreexd  17866  mreacs  17882  iscat  17896  iscatd  17897  iscatd2  17905  catcocl  17909  catpropd  17933  brssc  18039  issubc  18060  subcidcl  18069  subccocl  18070  isfunc  18089  isfuncd  18090  cofucl  18113  funcres2b  18122  fuciso  18203  yonedalem3  18504  yonffthlem  18506  ismgm  18867  ismgmd  18880  issstrmgm  18881  issgrpd  18969  ismndd  18996  eqgfval  19438  efgsdm  19995  efgsdmi  19997  efgsrel  19999  efgsp1  20002  efgsres  20003  dprdfcl  20280  ablfaclem3  20354  isdrngd  21073  isdrngdOLD  21075  issrng  21152  issrngd  21163  islmodd  21192  islbs  21402  lbsind  21406  lbspropd  21425  islbs2  21483  lbsextlem4  21490  lbsextg  21491  pzriprnglem8  21849  zndvds  21910  isphl  21989  isphld  22015  phlpropd  22016  frlmlbs  22158  islindf  22173  islinds2  22174  lindfind  22177  lindsind  22178  lindsind2  22180  lindfrn  22182  lindfmm  22188  lsslindf  22191  lindsenlbs  22212  mhppwdeg  22526  mat1dimmul  22846  istps  23307  tpspropd  23311  eltpsg  23316  islp  23513  1stcelcls  23835  kgeni  23911  kgencn2  23931  ptpjpre1  23945  elptr2  23948  ptbasin  23951  ptbasfi  23955  ptpjcn  23985  ptpjopn  23986  ptcld  23987  ptcldmpt  23988  ptclsg  23989  ptcnp  23996  qtopval  24069  ptcmplem2  24427  ptcmplem3  24428  ptcmplem4  24429  istmd  24448  istgp  24451  tmdgsum  24469  istlm  24559  isusp  24635  prdsdsf  24741  prdsxmet  24743  isms  24823  mspropd  24848  setsxms  24853  setsms  24854  tmsxms  24860  tmsms  24861  isnrg  25034  tngnrg  25048  bcthlem2  25701  bcthlem3  25702  bcthlem4  25703  bcthlem5  25704  iscms  25721  cmspropd  25725  cmssmscld  25726  cmsss  25727  shft2rab  25884  ovolicc2lem3  25895  ovolicc2lem4  25896  ovolicc2lem5  25897  vitalilem2  25985  vitalilem3  25986  vitali  25989  limcfval  26247  limcmpt2  26259  limcres  26261  cnplimc  26262  cnlimci  26264  elcpn  26309  uc1pval  26513  ig1pcl  26552  jensen  27373  axtgcont  28988  tglngval  29071  ishlg2  29122  ishlg  29125  mirbtwnb  29201  trgcopy  29368  trgcopyeu  29370  acopyeu  29399  isinagd  29415  tgasa1  29460  wlkp1lem3  30311  usgrwwlks2on  30604  umgrwwlks2on  30605  clwwlknon1  30745  clwwlknonclwlknonf1o  31020  imsmet  31350  smcn  31357  iscbn  31523  tgextahpl  33126  tgextancgra  33131  sbceqbidf  33182  fnpreimac  33362  isslmd  33862  0nellinds  34030  lindssn  34037  lindfpropd  34041  elrspunidl  34082  lbslsat  34359  lindsunlem  34367  brfldext  34388  submateq  34552  lmatcl  34559  ispcmp  34600  zarcmplem  34624  zhmnrg  34708  ismntoplly  34768  sigapildsys  34906  fiunelcarsg  35059  eulerpartlemgvv  35119  eulerpart  35125  fineqvinfep  35934  brlexod  36040  brr0d  36042  onvf1odlem2  36073  ptpconn  36206  cvmscbv  36231  cvmshmeo  36244  cvmsss2  36247  cvmliftlem7  36264  cvmliftlem10  36267  cvmlift2lem11  36286  cvmlift2lem12  36287  satffunlem1lem1  36375  satffunlem2lem1  36377  sategoelfvb  36392  prv1n  36404  elmpps  36546  mirimanoffr  36668  nmulprop  37154  nmulcom  37158  nmulrid  37161  nmuladdel  37176  cbvriotavw2  37240  cbvmpovw2  37246  cbvmpo1vw2  37247  cbvmpo2vw2  37248  cbvixpvw2  37249  cbvitgvw2  37252  cbvsbcdavw2  37262  cbvixpdavw  37282  cbvrmodavw2  37287  cbvreudavw2  37288  cbvmpodavw2  37295  cbvmpo1davw2  37296  cbvmpo2davw2  37297  cbvixpdavw2  37298  cbvproddavw2  37300  cbvitgdavw2  37301  weiunpo  37468  weiunso  37469  weiunfr  37470  weiunse  37471  bj-elabd2ALT  38053  bj-ru1  38071  currysetlem  38073  currysetlem1  38075  bj-ismoore  38296  csbfinxpg  38579  pibt2  38608  lindsadd  38804  ptrest  38805  upixp  38931  sdclem1  38943  sstotbnd2  38974  prdsbnd2  38995  isprrngo  39250  isopos  40503  isatl  40622  aks6d1c1p6  43430  isnacs3  43987  nacsfix  43989  mzpclall  44004  dnnumch1  44317  dnwech  44321  aomclem3  44324  aomclem8  44329  dfac11  44330  islmodfg  44337  oaordnr  44559  omnord1  44568  oenord1  44579  cantnfresb  44587  rfovcnvf1od  45265  ismnu  45506  sblpnf  45555  rusbcALT  45682  cbvrabv2w  46416  choicefi  46487  climsuselem1  46892  climsuse  46893  cncfuni  47169  dvnprodlem1  47229  stoweidlem31  47314  stoweidlem59  47342  fourierdlem46  47435  fourierdlem62  47451  fourierdlem72  47461  fourierdlem79  47468  fourierdlem88  47477  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem112  47501  qndenserrnbllem  47577  ioorrnopnlem  47587  ioorrnopn  47588  ioorrnopnxr  47590  issal  47597  subsaliuncllem  47640  subsaliuncl  47641  subsalsal  47642  sge0tsms  47663  sge0iunmpt  47701  sge0seq  47729  ovnsubaddlem1  47853  ovnsubaddlem2  47854  hoidmvlelem3  47880  hoidmvlelem4  47881  rrnmbl  47897  hoiqssbllem3  47907  hspmbl  47912  hoimbl  47914  issmflem  48010  issmfd  48018  issmfdf  48020  smfpimltmpt  48029  issmfled  48040  smfpimltxrmptf  48041  smfmbfcex  48043  issmfgtd  48044  smflimlem1  48054  smflimlem2  48055  smflimlem3  48056  smflimlem6  48059  smfpimgtmpt  48064  smfpimgtxrmptf  48067  smfres  48073  smfpimcclem  48090  smfpimcc  48091  dfateq12d  48469  iscllaw  49559  isprmrng  49764  islininds  49889  brab2ddw  50271  brab2ddw2  50272  funcf2lem  50526  isthincd2lem2  50901  setc1onsubc  51071