Theorem eleq12d 2827

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  neleq12d  3038  cbvraldva2  3315  cdeqel  3731  ruOLD  3736  sbceqbid  3744  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbcel12  4360  elvvuni  5698  elrnmpt1  5906  canth  7308  onnseq  8272  smoeq  8278  smores  8280  smores2  8282  iordsmo  8285  tz7.49  8372  nnaordr  8543  omsmolem  8580  naddel2  8611  fvixp  8834  cbvixp  8846  cbvixpv  8847  mptelixpg  8867  boxcutc  8873  ixpiunwdom  9485  elirr  9494  cantnflt  9571  oemapvali  9583  cantnflem1  9588  cantnf  9592  wemapwe  9596  cnfcom3lem  9602  ttrcltr  9615  rnttrcl  9621  infxpen  9914  dfac8alem  9929  dfac8clem  9932  ac5num  9936  acni2  9946  numacn  9949  acndom  9951  aceq3lem  10020  dfac5  10029  dfac9  10037  dfac13  10043  fin2i  10195  isfin2-2  10219  fin23lem27  10228  isfin3ds  10229  fin23lem17  10238  fin23lem39  10250  isf33lem  10266  isf34lem7  10279  isf34lem6  10280  fin1a2lem10  10309  fin1a2lem12  10311  hsmexlem4  10329  axcc2lem  10336  axcc3  10338  domtriomlem  10342  axdc2lem  10348  axdc3lem2  10351  axdc3lem3  10352  axdc3lem4  10353  axdc3  10354  axdc4lem  10355  axcclem  10357  ac6num  10379  ac6c4  10381  iundom2g  10440  fpwwe2  10543  pwfseqlem1  10558  pwfseqlem4a  10561  pwfseqlem4  10562  ltapi  10803  ltmpi  10804  fzsubel  13464  elfzp1b  13505  axdc4uzlem  13894  wrd2ind  14634  smuval  16396  prdsbasprj  17380  xpsfrnel  17470  ismri2dad  17547  mreexd  17552  mreacs  17568  iscat  17582  iscatd  17583  iscatd2  17591  catcocl  17595  catpropd  17619  brssc  17725  issubc  17746  subcidcl  17755  subccocl  17756  isfunc  17775  isfuncd  17776  cofucl  17799  funcres2b  17808  fuciso  17889  yonedalem3  18190  yonffthlem  18192  ismgm  18553  ismgmd  18564  issstrmgm  18565  issgrpd  18642  ismndd  18668  eqgfval  19092  efgsdm  19646  efgsdmi  19648  efgsrel  19650  efgsp1  19653  efgsres  19654  dprdfcl  19931  ablfaclem3  20005  isdrngd  20684  isdrngdOLD  20686  issrng  20763  issrngd  20774  islmodd  20803  islbs  21014  lbsind  21018  lbspropd  21037  islbs2  21095  lbsextlem4  21102  lbsextg  21103  pzriprnglem8  21429  zndvds  21490  isphl  21569  isphld  21595  phlpropd  21596  frlmlbs  21738  islindf  21753  islinds2  21754  lindfind  21757  lindsind  21758  lindsind2  21760  lindfrn  21762  lindfmm  21768  lsslindf  21771  mhppwdeg  22068  mat1dimmul  22394  istps  22852  tpspropd  22856  eltpsg  22861  islp  23058  1stcelcls  23379  kgeni  23455  kgencn2  23475  ptpjpre1  23489  elptr2  23492  ptbasin  23495  ptbasfi  23499  ptpjcn  23529  ptpjopn  23530  ptcld  23531  ptcldmpt  23532  ptclsg  23533  ptcnp  23540  qtopval  23613  ptcmplem2  23971  ptcmplem3  23972  ptcmplem4  23973  istmd  23992  istgp  23995  tmdgsum  24013  istlm  24103  isusp  24179  prdsdsf  24285  prdsxmet  24287  isms  24367  mspropd  24392  setsxms  24397  setsms  24398  tmsxms  24404  tmsms  24405  isnrg  24578  tngnrg  24592  bcthlem2  25255  bcthlem3  25256  bcthlem4  25257  bcthlem5  25258  iscms  25275  cmspropd  25279  cmssmscld  25280  cmsss  25281  shft2rab  25439  ovolicc2lem3  25450  ovolicc2lem4  25451  ovolicc2lem5  25452  vitalilem2  25540  vitalilem3  25541  vitali  25544  limcfval  25803  limcmpt2  25815  limcres  25817  cnplimc  25818  cnlimci  25820  elcpn  25866  uc1pval  26075  ig1pcl  26114  jensen  26929  axtgcont  28450  tglngval  28532  ishlg  28583  mirbtwnb  28653  trgcopy  28785  trgcopyeu  28787  acopyeu  28815  isinagd  28820  tgasa1  28839  wlkp1lem3  29656  usgrwwlks2on  29940  umgrwwlks2on  29941  clwwlknon1  30081  clwwlknonclwlknonf1o  30346  imsmet  30675  smcn  30682  iscbn  30848  sbceqbidf  32470  fnpreimac  32657  isslmd  33180  0nellinds  33344  lindssn  33352  lindfpropd  33356  elrspunidl  33402  lbslsat  33652  lindsunlem  33660  brfldext  33681  submateq  33845  lmatcl  33852  ispcmp  33893  zarcmplem  33917  zhmnrg  34001  ismntoplly  34061  sigapildsys  34198  fiunelcarsg  34352  eulerpartlemgvv  34412  eulerpart  34418  onvf1odlem2  35171  ptpconn  35300  cvmscbv  35325  cvmshmeo  35338  cvmsss2  35341  cvmliftlem7  35358  cvmliftlem10  35361  cvmlift2lem11  35380  cvmlift2lem12  35381  satffunlem1lem1  35469  satffunlem2lem1  35471  sategoelfvb  35486  prv1n  35498  elmpps  35640  cbvriotavw2  36303  cbvmpovw2  36309  cbvmpo1vw2  36310  cbvmpo2vw2  36311  cbvixpvw2  36312  cbvitgvw2  36315  cbvsbcdavw2  36325  cbvixpdavw  36345  cbvrmodavw2  36350  cbvreudavw2  36351  cbvmpodavw2  36358  cbvmpo1davw2  36359  cbvmpo2davw2  36360  cbvixpdavw2  36361  cbvproddavw2  36363  cbvitgdavw2  36364  weiunpo  36532  weiunso  36533  weiunfr  36534  weiunse  36535  bj-elabd2ALT  36992  bj-ru1  37010  currysetlem  37012  currysetlem1  37014  bj-ismoore  37172  csbfinxpg  37455  pibt2  37484  lindsadd  37676  lindsenlbs  37678  ptrest  37682  upixp  37792  sdclem1  37806  sstotbnd2  37837  prdsbnd2  37858  isprrngo  38113  isopos  39302  isatl  39421  aks6d1c1p6  42230  isnacs3  42830  nacsfix  42832  mzpclall  42847  dnnumch1  43164  dnwech  43168  aomclem3  43176  aomclem8  43181  dfac11  43182  islmodfg  43189  oaordnr  43416  omnord1  43425  oenord1  43436  cantnfresb  43444  rfovcnvf1od  44124  ismnu  44381  sblpnf  44430  rusbcALT  44558  cbvrabv2w  45252  choicefi  45324  climsuselem1  45734  climsuse  45735  cncfuni  46011  dvnprodlem1  46071  stoweidlem31  46156  stoweidlem59  46184  fourierdlem46  46277  fourierdlem62  46293  fourierdlem72  46303  fourierdlem79  46310  fourierdlem88  46319  fourierdlem89  46320  fourierdlem90  46321  fourierdlem91  46322  fourierdlem112  46343  qndenserrnbllem  46419  ioorrnopnlem  46429  ioorrnopn  46430  ioorrnopnxr  46432  issal  46439  subsaliuncllem  46482  subsaliuncl  46483  subsalsal  46484  sge0tsms  46505  sge0iunmpt  46543  sge0seq  46571  ovnsubaddlem1  46695  ovnsubaddlem2  46696  hoidmvlelem3  46722  hoidmvlelem4  46723  rrnmbl  46739  hoiqssbllem3  46749  hspmbl  46754  hoimbl  46756  issmflem  46852  issmfd  46860  issmfdf  46862  smfpimltmpt  46871  issmfled  46882  smfpimltxrmptf  46883  smfmbfcex  46885  issmfgtd  46886  smflimlem1  46896  smflimlem2  46897  smflimlem3  46898  smflimlem6  46901  smfpimgtmpt  46906  smfpimgtxrmptf  46909  smfres  46915  smfpimcclem  46932  smfpimcc  46933  dfateq12d  47253  iscllaw  48316  islininds  48574  brab2ddw  48956  brab2ddw2  48957  funcf2lem  49209  isthincd2lem2  49563  setc1onsubc  49730