Theorem eleq12d 2828

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  neleq12d  3052  cbvraldva2  3345  cbvrexdva2OLD  3347  cdeqel  3773  ru  3777  sbceqbid  3785  cbvrabcsfw  3938  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  sbcel12  4409  elvvuni  5753  elrnmpt1  5958  canth  7362  onnseq  8344  smoeq  8350  smores  8352  smores2  8354  iordsmo  8357  tz7.49  8445  nnaordr  8620  omsmolem  8656  naddel2  8687  fvixp  8896  cbvixp  8908  mptelixpg  8929  boxcutc  8935  ixpiunwdom  9585  elirr  9592  cantnflt  9667  oemapvali  9679  cantnflem1  9684  cantnf  9688  wemapwe  9692  cnfcom3lem  9698  ttrcltr  9711  rnttrcl  9717  infxpen  10009  dfac8alem  10024  dfac8clem  10027  ac5num  10031  acni2  10041  numacn  10044  acndom  10046  aceq3lem  10115  dfac5  10123  dfac9  10131  dfac13  10137  fin2i  10290  isfin2-2  10314  fin23lem27  10323  isfin3ds  10324  fin23lem17  10333  fin23lem39  10345  isf33lem  10361  isf34lem7  10374  isf34lem6  10375  fin1a2lem10  10404  fin1a2lem12  10406  hsmexlem4  10424  axcc2lem  10431  axcc3  10433  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc3lem3  10447  axdc3lem4  10448  axdc3  10449  axdc4lem  10450  axcclem  10452  ac6num  10474  ac6c4  10476  iundom2g  10535  fpwwe2  10638  pwfseqlem1  10653  pwfseqlem4a  10656  pwfseqlem4  10657  ltapi  10898  ltmpi  10899  eluzaddOLD  12857  fzsubel  13537  elfzp1b  13578  axdc4uzlem  13948  wrd2ind  14673  smuval  16422  prdsbasprj  17418  xpsfrnel  17508  ismri2dad  17581  mreexd  17586  mreacs  17602  iscat  17616  iscatd  17617  iscatd2  17625  catcocl  17629  catpropd  17653  brssc  17761  issubc  17785  subcidcl  17794  subccocl  17795  isfunc  17814  isfuncd  17815  cofucl  17838  funcres2b  17847  fuciso  17928  yonedalem3  18233  yonffthlem  18235  ismgm  18562  issstrmgm  18572  issgrpd  18621  ismndd  18647  eqgfval  19056  efgsdm  19598  efgsdmi  19600  efgsrel  19602  efgsp1  19605  efgsres  19606  dprdfcl  19883  ablfaclem3  19957  isdrngd  20390  isdrngdOLD  20392  issrng  20458  issrngd  20469  islmodd  20477  islbs  20687  lbsind  20691  lbspropd  20710  islbs2  20767  lbsextlem4  20774  lbsextg  20775  zndvds  21105  isphl  21181  isphld  21207  phlpropd  21208  frlmlbs  21352  islindf  21367  islinds2  21368  lindfind  21371  lindsind  21372  lindsind2  21374  lindfrn  21376  lindfmm  21382  lsslindf  21385  mhppwdeg  21693  mat1dimmul  21978  istps  22436  tpspropd  22440  eltpsg  22445  eltpsgOLD  22446  islp  22644  1stcelcls  22965  kgeni  23041  kgencn2  23061  ptpjpre1  23075  elptr2  23078  ptbasin  23081  ptbasfi  23085  ptpjcn  23115  ptpjopn  23116  ptcld  23117  ptcldmpt  23118  ptclsg  23119  ptcnp  23126  qtopval  23199  ptcmplem2  23557  ptcmplem3  23558  ptcmplem4  23559  istmd  23578  istgp  23581  tmdgsum  23599  istlm  23689  isusp  23766  prdsdsf  23873  prdsxmet  23875  isms  23955  mspropd  23980  setsxms  23987  setsms  23988  tmsxms  23995  tmsms  23996  isnrg  24177  tngnrg  24191  bcthlem2  24842  bcthlem3  24843  bcthlem4  24844  bcthlem5  24845  iscms  24862  cmspropd  24866  cmssmscld  24867  cmsss  24868  shft2rab  25025  ovolicc2lem3  25036  ovolicc2lem4  25037  ovolicc2lem5  25038  vitalilem2  25126  vitalilem3  25127  vitali  25130  limcfval  25389  limcmpt2  25401  limcres  25403  cnplimc  25404  cnlimci  25406  elcpn  25451  uc1pval  25657  ig1pcl  25693  jensen  26493  axtgcont  27720  tglngval  27802  ishlg  27853  mirbtwnb  27923  trgcopy  28055  trgcopyeu  28057  acopyeu  28085  isinagd  28090  tgasa1  28109  wlkp1lem3  28932  umgrwwlks2on  29211  clwwlknon1  29350  clwwlknonclwlknonf1o  29615  imsmet  29944  smcn  29951  iscbn  30117  sbceqbidf  31727  fnpreimac  31896  isslmd  32347  0nellinds  32483  lindssn  32494  lindfpropd  32498  elrspunidl  32546  lbslsat  32701  lindsunlem  32709  brfldext  32726  submateq  32789  lmatcl  32796  ispcmp  32837  zarcmplem  32861  zhmnrg  32947  ismntoplly  33005  sigapildsys  33160  fiunelcarsg  33315  eulerpartlemgvv  33375  eulerpart  33381  ptpconn  34224  cvmscbv  34249  cvmshmeo  34262  cvmsss2  34265  cvmliftlem7  34282  cvmliftlem10  34285  cvmlift2lem11  34304  cvmlift2lem12  34305  satffunlem1lem1  34393  satffunlem2lem1  34395  sategoelfvb  34410  prv1n  34422  elmpps  34564  bj-elabd2ALT  35805  currysetlem  35826  currysetlem1  35828  bj-ismoore  35986  csbfinxpg  36269  pibt2  36298  lindsadd  36481  lindsenlbs  36483  ptrest  36487  upixp  36597  sdclem1  36611  sstotbnd2  36642  prdsbnd2  36663  isprrngo  36918  isopos  38050  isatl  38169  isnacs3  41448  nacsfix  41450  mzpclall  41465  dnnumch1  41786  dnwech  41790  aomclem3  41798  aomclem8  41803  dfac11  41804  islmodfg  41811  oaordnr  42046  omnord1  42055  oenord1  42066  cantnfresb  42074  rfovcnvf1od  42755  ismnu  43020  sblpnf  43069  rusbcALT  43198  choicefi  43899  climsuselem1  44323  climsuse  44324  cncfuni  44602  dvnprodlem1  44662  stoweidlem31  44747  stoweidlem59  44775  fourierdlem46  44868  fourierdlem62  44884  fourierdlem72  44894  fourierdlem79  44901  fourierdlem88  44910  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem112  44934  qndenserrnbllem  45010  ioorrnopnlem  45020  ioorrnopn  45021  ioorrnopnxr  45023  issal  45030  subsaliuncllem  45073  subsaliuncl  45074  subsalsal  45075  sge0tsms  45096  sge0iunmpt  45134  sge0seq  45162  ovnsubaddlem1  45286  ovnsubaddlem2  45287  hoidmvlelem3  45313  hoidmvlelem4  45314  rrnmbl  45330  hoiqssbllem3  45340  hspmbl  45345  hoimbl  45347  issmflem  45443  issmfd  45451  issmfdf  45453  smfpimltmpt  45462  issmfled  45473  smfpimltxrmptf  45474  smfmbfcex  45476  issmfgtd  45477  smflimlem1  45487  smflimlem2  45488  smflimlem3  45489  smflimlem6  45492  smfpimgtmpt  45497  smfpimgtxrmptf  45500  smfres  45506  smfpimcclem  45523  smfpimcc  45524  dfateq12d  45834  ismgmd  46546  iscllaw  46599  pzriprnglem8  46812  islininds  47127  funcf2lem  47638  isthincd2lem2  47656