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 278	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  neleq12d  3051  cbvraldva2  3344  cbvrexdva2OLD  3346  cdeqel  3772  ru  3776  sbceqbid  3784  cbvrabcsfw  3937  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  sbcel12  4408  elvvuni  5752  elrnmpt1  5957  canth  7364  onnseq  8346  smoeq  8352  smores  8354  smores2  8356  iordsmo  8359  tz7.49  8447  nnaordr  8622  omsmolem  8658  naddel2  8689  fvixp  8898  cbvixp  8910  mptelixpg  8931  boxcutc  8937  ixpiunwdom  9587  elirr  9594  cantnflt  9669  oemapvali  9681  cantnflem1  9686  cantnf  9690  wemapwe  9694  cnfcom3lem  9700  ttrcltr  9713  rnttrcl  9719  infxpen  10011  dfac8alem  10026  dfac8clem  10029  ac5num  10033  acni2  10043  numacn  10046  acndom  10048  aceq3lem  10117  dfac5  10125  dfac9  10133  dfac13  10139  fin2i  10292  isfin2-2  10316  fin23lem27  10325  isfin3ds  10326  fin23lem17  10335  fin23lem39  10347  isf33lem  10363  isf34lem7  10376  isf34lem6  10377  fin1a2lem10  10406  fin1a2lem12  10408  hsmexlem4  10426  axcc2lem  10433  axcc3  10435  domtriomlem  10439  axdc2lem  10445  axdc3lem2  10448  axdc3lem3  10449  axdc3lem4  10450  axdc3  10451  axdc4lem  10452  axcclem  10454  ac6num  10476  ac6c4  10478  iundom2g  10537  fpwwe2  10640  pwfseqlem1  10655  pwfseqlem4a  10658  pwfseqlem4  10659  ltapi  10900  ltmpi  10901  eluzaddOLD  12859  fzsubel  13539  elfzp1b  13580  axdc4uzlem  13950  wrd2ind  14675  smuval  16424  prdsbasprj  17420  xpsfrnel  17510  ismri2dad  17583  mreexd  17588  mreacs  17604  iscat  17618  iscatd  17619  iscatd2  17627  catcocl  17631  catpropd  17655  brssc  17763  issubc  17787  subcidcl  17796  subccocl  17797  isfunc  17816  isfuncd  17817  cofucl  17840  funcres2b  17849  fuciso  17930  yonedalem3  18235  yonffthlem  18237  ismgm  18564  issstrmgm  18574  issgrpd  18623  ismndd  18649  eqgfval  19058  efgsdm  19600  efgsdmi  19602  efgsrel  19604  efgsp1  19607  efgsres  19608  dprdfcl  19885  ablfaclem3  19959  isdrngd  20394  isdrngdOLD  20396  issrng  20462  issrngd  20473  islmodd  20481  islbs  20692  lbsind  20696  lbspropd  20715  islbs2  20773  lbsextlem4  20780  lbsextg  20781  zndvds  21111  isphl  21187  isphld  21213  phlpropd  21214  frlmlbs  21358  islindf  21373  islinds2  21374  lindfind  21377  lindsind  21378  lindsind2  21380  lindfrn  21382  lindfmm  21388  lsslindf  21391  mhppwdeg  21699  mat1dimmul  21985  istps  22443  tpspropd  22447  eltpsg  22452  eltpsgOLD  22453  islp  22651  1stcelcls  22972  kgeni  23048  kgencn2  23068  ptpjpre1  23082  elptr2  23085  ptbasin  23088  ptbasfi  23092  ptpjcn  23122  ptpjopn  23123  ptcld  23124  ptcldmpt  23125  ptclsg  23126  ptcnp  23133  qtopval  23206  ptcmplem2  23564  ptcmplem3  23565  ptcmplem4  23566  istmd  23585  istgp  23588  tmdgsum  23606  istlm  23696  isusp  23773  prdsdsf  23880  prdsxmet  23882  isms  23962  mspropd  23987  setsxms  23994  setsms  23995  tmsxms  24002  tmsms  24003  isnrg  24184  tngnrg  24198  bcthlem2  24849  bcthlem3  24850  bcthlem4  24851  bcthlem5  24852  iscms  24869  cmspropd  24873  cmssmscld  24874  cmsss  24875  shft2rab  25032  ovolicc2lem3  25043  ovolicc2lem4  25044  ovolicc2lem5  25045  vitalilem2  25133  vitalilem3  25134  vitali  25137  limcfval  25396  limcmpt2  25408  limcres  25410  cnplimc  25411  cnlimci  25413  elcpn  25458  uc1pval  25664  ig1pcl  25700  jensen  26500  axtgcont  27758  tglngval  27840  ishlg  27891  mirbtwnb  27961  trgcopy  28093  trgcopyeu  28095  acopyeu  28123  isinagd  28128  tgasa1  28147  wlkp1lem3  28970  umgrwwlks2on  29249  clwwlknon1  29388  clwwlknonclwlknonf1o  29653  imsmet  29982  smcn  29989  iscbn  30155  sbceqbidf  31765  fnpreimac  31934  isslmd  32388  0nellinds  32528  lindssn  32539  lindfpropd  32543  elrspunidl  32591  lbslsat  32760  lindsunlem  32768  brfldext  32785  submateq  32858  lmatcl  32865  ispcmp  32906  zarcmplem  32930  zhmnrg  33016  ismntoplly  33074  sigapildsys  33229  fiunelcarsg  33384  eulerpartlemgvv  33444  eulerpart  33450  ptpconn  34293  cvmscbv  34318  cvmshmeo  34331  cvmsss2  34334  cvmliftlem7  34351  cvmliftlem10  34354  cvmlift2lem11  34373  cvmlift2lem12  34374  satffunlem1lem1  34462  satffunlem2lem1  34464  sategoelfvb  34479  prv1n  34491  elmpps  34633  bj-elabd2ALT  35891  currysetlem  35912  currysetlem1  35914  bj-ismoore  36072  csbfinxpg  36355  pibt2  36384  lindsadd  36567  lindsenlbs  36569  ptrest  36573  upixp  36683  sdclem1  36697  sstotbnd2  36728  prdsbnd2  36749  isprrngo  37004  isopos  38136  isatl  38255  isnacs3  41530  nacsfix  41532  mzpclall  41547  dnnumch1  41868  dnwech  41872  aomclem3  41880  aomclem8  41885  dfac11  41886  islmodfg  41893  oaordnr  42128  omnord1  42137  oenord1  42148  cantnfresb  42156  rfovcnvf1od  42837  ismnu  43102  sblpnf  43151  rusbcALT  43280  choicefi  43978  climsuselem1  44402  climsuse  44403  cncfuni  44681  dvnprodlem1  44741  stoweidlem31  44826  stoweidlem59  44854  fourierdlem46  44947  fourierdlem62  44963  fourierdlem72  44973  fourierdlem79  44980  fourierdlem88  44989  fourierdlem89  44990  fourierdlem90  44991  fourierdlem91  44992  fourierdlem112  45013  qndenserrnbllem  45089  ioorrnopnlem  45099  ioorrnopn  45100  ioorrnopnxr  45102  issal  45109  subsaliuncllem  45152  subsaliuncl  45153  subsalsal  45154  sge0tsms  45175  sge0iunmpt  45213  sge0seq  45241  ovnsubaddlem1  45365  ovnsubaddlem2  45366  hoidmvlelem3  45392  hoidmvlelem4  45393  rrnmbl  45409  hoiqssbllem3  45419  hspmbl  45424  hoimbl  45426  issmflem  45522  issmfd  45530  issmfdf  45532  smfpimltmpt  45541  issmfled  45552  smfpimltxrmptf  45553  smfmbfcex  45555  issmfgtd  45556  smflimlem1  45566  smflimlem2  45567  smflimlem3  45568  smflimlem6  45571  smfpimgtmpt  45576  smfpimgtxrmptf  45579  smfres  45585  smfpimcclem  45602  smfpimcc  45603  dfateq12d  45913  ismgmd  46625  iscllaw  46678  pzriprnglem8  46891  islininds  47205  funcf2lem  47716  isthincd2lem2  47734