Theorem eleq12d 2822

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  neleq12d  3034  cbvraldva2  3312  cbvrexdva2OLD  3314  cdeqel  3738  ruOLD  3743  sbceqbid  3751  cbvrabcsfw  3894  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbcel12  4364  elvvuni  5700  elrnmpt1  5906  canth  7307  onnseq  8274  smoeq  8280  smores  8282  smores2  8284  iordsmo  8287  tz7.49  8374  nnaordr  8545  omsmolem  8582  naddel2  8613  fvixp  8836  cbvixp  8848  cbvixpv  8849  mptelixpg  8869  boxcutc  8875  ixpiunwdom  9501  elirr  9510  cantnflt  9587  oemapvali  9599  cantnflem1  9604  cantnf  9608  wemapwe  9612  cnfcom3lem  9618  ttrcltr  9631  rnttrcl  9637  infxpen  9927  dfac8alem  9942  dfac8clem  9945  ac5num  9949  acni2  9959  numacn  9962  acndom  9964  aceq3lem  10033  dfac5  10042  dfac9  10050  dfac13  10056  fin2i  10208  isfin2-2  10232  fin23lem27  10241  isfin3ds  10242  fin23lem17  10251  fin23lem39  10263  isf33lem  10279  isf34lem7  10292  isf34lem6  10293  fin1a2lem10  10322  fin1a2lem12  10324  hsmexlem4  10342  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3lem4  10366  axdc3  10367  axdc4lem  10368  axcclem  10370  ac6num  10392  ac6c4  10394  iundom2g  10453  fpwwe2  10556  pwfseqlem1  10571  pwfseqlem4a  10574  pwfseqlem4  10575  ltapi  10816  ltmpi  10817  eluzaddOLD  12788  fzsubel  13481  elfzp1b  13522  axdc4uzlem  13908  wrd2ind  14647  smuval  16410  prdsbasprj  17394  xpsfrnel  17484  ismri2dad  17561  mreexd  17566  mreacs  17582  iscat  17596  iscatd  17597  iscatd2  17605  catcocl  17609  catpropd  17633  brssc  17739  issubc  17760  subcidcl  17769  subccocl  17770  isfunc  17789  isfuncd  17790  cofucl  17813  funcres2b  17822  fuciso  17903  yonedalem3  18204  yonffthlem  18206  ismgm  18533  ismgmd  18544  issstrmgm  18545  issgrpd  18622  ismndd  18648  eqgfval  19073  efgsdm  19627  efgsdmi  19629  efgsrel  19631  efgsp1  19634  efgsres  19635  dprdfcl  19912  ablfaclem3  19986  isdrngd  20668  isdrngdOLD  20670  issrng  20747  issrngd  20758  islmodd  20787  islbs  20998  lbsind  21002  lbspropd  21021  islbs2  21079  lbsextlem4  21086  lbsextg  21087  pzriprnglem8  21413  zndvds  21474  isphl  21553  isphld  21579  phlpropd  21580  frlmlbs  21722  islindf  21737  islinds2  21738  lindfind  21741  lindsind  21742  lindsind2  21744  lindfrn  21746  lindfmm  21752  lsslindf  21755  mhppwdeg  22053  mat1dimmul  22379  istps  22837  tpspropd  22841  eltpsg  22846  islp  23043  1stcelcls  23364  kgeni  23440  kgencn2  23460  ptpjpre1  23474  elptr2  23477  ptbasin  23480  ptbasfi  23484  ptpjcn  23514  ptpjopn  23515  ptcld  23516  ptcldmpt  23517  ptclsg  23518  ptcnp  23525  qtopval  23598  ptcmplem2  23956  ptcmplem3  23957  ptcmplem4  23958  istmd  23977  istgp  23980  tmdgsum  23998  istlm  24088  isusp  24165  prdsdsf  24271  prdsxmet  24273  isms  24353  mspropd  24378  setsxms  24383  setsms  24384  tmsxms  24390  tmsms  24391  isnrg  24564  tngnrg  24578  bcthlem2  25241  bcthlem3  25242  bcthlem4  25243  bcthlem5  25244  iscms  25261  cmspropd  25265  cmssmscld  25266  cmsss  25267  shft2rab  25425  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2lem5  25438  vitalilem2  25526  vitalilem3  25527  vitali  25530  limcfval  25789  limcmpt2  25801  limcres  25803  cnplimc  25804  cnlimci  25806  elcpn  25852  uc1pval  26061  ig1pcl  26100  jensen  26915  axtgcont  28432  tglngval  28514  ishlg  28565  mirbtwnb  28635  trgcopy  28767  trgcopyeu  28769  acopyeu  28797  isinagd  28802  tgasa1  28821  wlkp1lem3  29637  umgrwwlks2on  29920  clwwlknon1  30059  clwwlknonclwlknonf1o  30324  imsmet  30653  smcn  30660  iscbn  30826  sbceqbidf  32449  fnpreimac  32628  isslmd  33157  0nellinds  33320  lindssn  33328  lindfpropd  33332  elrspunidl  33378  lbslsat  33591  lindsunlem  33599  brfldext  33620  submateq  33778  lmatcl  33785  ispcmp  33826  zarcmplem  33850  zhmnrg  33934  ismntoplly  33994  sigapildsys  34131  fiunelcarsg  34286  eulerpartlemgvv  34346  eulerpart  34352  onvf1odlem2  35079  ptpconn  35208  cvmscbv  35233  cvmshmeo  35246  cvmsss2  35249  cvmliftlem7  35266  cvmliftlem10  35269  cvmlift2lem11  35288  cvmlift2lem12  35289  satffunlem1lem1  35377  satffunlem2lem1  35379  sategoelfvb  35394  prv1n  35406  elmpps  35548  cbvriotavw2  36212  cbvmpovw2  36218  cbvmpo1vw2  36219  cbvmpo2vw2  36220  cbvixpvw2  36221  cbvitgvw2  36224  cbvsbcdavw2  36234  cbvixpdavw  36254  cbvrmodavw2  36259  cbvreudavw2  36260  cbvmpodavw2  36267  cbvmpo1davw2  36268  cbvmpo2davw2  36269  cbvixpdavw2  36270  cbvproddavw2  36272  cbvitgdavw2  36273  weiunpo  36441  weiunso  36442  weiunfr  36443  weiunse  36444  bj-elabd2ALT  36901  bj-ru1  36919  currysetlem  36921  currysetlem1  36923  bj-ismoore  37081  csbfinxpg  37364  pibt2  37393  lindsadd  37595  lindsenlbs  37597  ptrest  37601  upixp  37711  sdclem1  37725  sstotbnd2  37756  prdsbnd2  37777  isprrngo  38032  isopos  39161  isatl  39280  aks6d1c1p6  42090  isnacs3  42686  nacsfix  42688  mzpclall  42703  dnnumch1  43020  dnwech  43024  aomclem3  43032  aomclem8  43037  dfac11  43038  islmodfg  43045  oaordnr  43272  omnord1  43281  oenord1  43292  cantnfresb  43300  rfovcnvf1od  43980  ismnu  44237  sblpnf  44286  rusbcALT  44415  cbvrabv2w  45109  choicefi  45181  climsuselem1  45592  climsuse  45593  cncfuni  45871  dvnprodlem1  45931  stoweidlem31  46016  stoweidlem59  46044  fourierdlem46  46137  fourierdlem62  46153  fourierdlem72  46163  fourierdlem79  46170  fourierdlem88  46179  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem112  46203  qndenserrnbllem  46279  ioorrnopnlem  46289  ioorrnopn  46290  ioorrnopnxr  46292  issal  46299  subsaliuncllem  46342  subsaliuncl  46343  subsalsal  46344  sge0tsms  46365  sge0iunmpt  46403  sge0seq  46431  ovnsubaddlem1  46555  ovnsubaddlem2  46556  hoidmvlelem3  46582  hoidmvlelem4  46583  rrnmbl  46599  hoiqssbllem3  46609  hspmbl  46614  hoimbl  46616  issmflem  46712  issmfd  46720  issmfdf  46722  smfpimltmpt  46731  issmfled  46742  smfpimltxrmptf  46743  smfmbfcex  46745  issmfgtd  46746  smflimlem1  46756  smflimlem2  46757  smflimlem3  46758  smflimlem6  46761  smfpimgtmpt  46766  smfpimgtxrmptf  46769  smfres  46775  smfpimcclem  46792  smfpimcc  46793  dfateq12d  47114  iscllaw  48177  islininds  48435  brab2ddw  48817  brab2ddw2  48818  funcf2lem  49070  isthincd2lem2  49424  setc1onsubc  49591