Theorem eleq12d 2834

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ 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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  neleq12d  3054  cbvraldva2  3393  cbvrexdva2  3394  cdeqel  3712  ru  3716  sbceqbid  3724  cbvrabcsfw  3877  cbvralcsf  3878  cbvreucsf  3880  cbvrabcsf  3881  sbcel12  4343  elvvuni  5664  elrnmpt1  5870  canth  7238  onnseq  8184  smoeq  8190  smores  8192  smores2  8194  iordsmo  8197  tz7.49  8285  nnaordr  8460  omsmolem  8496  fvixp  8699  cbvixp  8711  mptelixpg  8732  boxcutc  8738  ixpiunwdom  9358  elirr  9365  cantnflt  9439  oemapvali  9451  cantnflem1  9456  cantnf  9460  wemapwe  9464  cnfcom3lem  9470  ttrcltr  9483  rnttrcl  9489  infxpen  9779  dfac8alem  9794  dfac8clem  9797  ac5num  9801  acni2  9811  numacn  9814  acndom  9816  aceq3lem  9885  dfac5  9893  dfac9  9901  dfac13  9907  fin2i  10060  isfin2-2  10084  fin23lem27  10093  isfin3ds  10094  fin23lem17  10103  fin23lem39  10115  isf33lem  10131  isf34lem7  10144  isf34lem6  10145  fin1a2lem10  10174  fin1a2lem12  10176  hsmexlem4  10194  axcc2lem  10201  axcc3  10203  domtriomlem  10207  axdc2lem  10213  axdc3lem2  10216  axdc3lem3  10217  axdc3lem4  10218  axdc3  10219  axdc4lem  10220  axcclem  10222  ac6num  10244  ac6c4  10246  iundom2g  10305  fpwwe2  10408  pwfseqlem1  10423  pwfseqlem4a  10426  pwfseqlem4  10427  ltapi  10668  ltmpi  10669  eluzadd  12622  fzsubel  13301  elfzp1b  13342  axdc4uzlem  13712  wrd2ind  14445  smuval  16197  prdsbasprj  17192  xpsfrnel  17282  ismri2dad  17355  mreexd  17360  mreacs  17376  iscat  17390  iscatd  17391  iscatd2  17399  catcocl  17403  catpropd  17427  brssc  17535  issubc  17559  subcidcl  17568  subccocl  17569  isfunc  17588  isfuncd  17589  cofucl  17612  funcres2b  17621  fuciso  17702  yonedalem3  18007  yonffthlem  18009  ismgm  18336  issstrmgm  18346  ismndd  18416  eqgfval  18813  efgsdm  19345  efgsdmi  19347  efgsrel  19349  efgsp1  19352  efgsres  19353  dprdfcl  19625  ablfaclem3  19699  isdrngd  20025  issrng  20119  issrngd  20130  islmodd  20138  islbs  20347  lbsind  20351  lbspropd  20370  islbs2  20425  lbsextlem4  20432  lbsextg  20433  zndvds  20766  isphl  20842  isphld  20868  phlpropd  20869  frlmlbs  21013  islindf  21028  islinds2  21029  lindfind  21032  lindsind  21033  lindsind2  21035  lindfrn  21037  lindfmm  21043  lsslindf  21046  mhppwdeg  21349  mat1dimmul  21634  istps  22092  tpspropd  22096  eltpsg  22101  eltpsgOLD  22102  islp  22300  1stcelcls  22621  kgeni  22697  kgencn2  22717  ptpjpre1  22731  elptr2  22734  ptbasin  22737  ptbasfi  22741  ptpjcn  22771  ptpjopn  22772  ptcld  22773  ptcldmpt  22774  ptclsg  22775  ptcnp  22782  qtopval  22855  ptcmplem2  23213  ptcmplem3  23214  ptcmplem4  23215  istmd  23234  istgp  23237  tmdgsum  23255  istlm  23345  isusp  23422  prdsdsf  23529  prdsxmet  23531  isms  23611  mspropd  23636  setsxms  23643  setsms  23644  tmsxms  23651  tmsms  23652  isnrg  23833  tngnrg  23847  bcthlem2  24498  bcthlem3  24499  bcthlem4  24500  bcthlem5  24501  iscms  24518  cmspropd  24522  cmssmscld  24523  cmsss  24524  shft2rab  24681  ovolicc2lem3  24692  ovolicc2lem4  24693  ovolicc2lem5  24694  vitalilem2  24782  vitalilem3  24783  vitali  24786  limcfval  25045  limcmpt2  25057  limcres  25059  cnplimc  25060  cnlimci  25062  elcpn  25107  uc1pval  25313  ig1pcl  25349  jensen  26147  axtgcont  26839  tglngval  26921  ishlg  26972  mirbtwnb  27042  trgcopy  27174  trgcopyeu  27176  acopyeu  27204  isinagd  27209  tgasa1  27228  wlkp1lem3  28052  umgrwwlks2on  28331  clwwlknon1  28470  clwwlknonclwlknonf1o  28735  imsmet  29062  smcn  29069  iscbn  29235  sbceqbidf  30844  fnpreimac  31017  isslmd  31464  0nellinds  31575  lindssn  31582  lindfpropd  31585  elrspunidl  31615  lbslsat  31708  lindsunlem  31714  brfldext  31731  submateq  31768  lmatcl  31775  ispcmp  31816  zarcmplem  31840  zhmnrg  31926  ismntoplly  31984  sigapildsys  32139  fiunelcarsg  32292  eulerpartlemgvv  32352  eulerpart  32358  ptpconn  33204  cvmscbv  33229  cvmshmeo  33242  cvmsss2  33245  cvmliftlem7  33262  cvmliftlem10  33265  cvmlift2lem11  33284  cvmlift2lem12  33285  satffunlem1lem1  33373  satffunlem2lem1  33375  sategoelfvb  33390  prv1n  33402  elmpps  33544  naddel2  33849  bj-elabd2ALT  35122  currysetlem  35143  currysetlem1  35145  bj-ismoore  35285  csbfinxpg  35568  pibt2  35597  lindsadd  35779  lindsenlbs  35781  ptrest  35785  upixp  35896  sdclem1  35910  sstotbnd2  35941  prdsbnd2  35962  isprrngo  36217  isopos  37201  isatl  37320  isnacs3  40539  nacsfix  40541  mzpclall  40556  dnnumch1  40876  dnwech  40880  aomclem3  40888  aomclem8  40893  dfac11  40894  islmodfg  40901  rfovcnvf1od  41619  ismnu  41886  sblpnf  41935  rusbcALT  42064  choicefi  42747  climsuselem1  43155  climsuse  43156  cncfuni  43434  dvnprodlem1  43494  stoweidlem31  43579  stoweidlem59  43607  fourierdlem46  43700  fourierdlem62  43716  fourierdlem72  43726  fourierdlem79  43733  fourierdlem88  43742  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem112  43766  qndenserrnbllem  43842  ioorrnopnlem  43852  ioorrnopn  43853  ioorrnopnxr  43855  issal  43862  subsaliuncllem  43903  subsaliuncl  43904  subsalsal  43905  sge0tsms  43925  sge0iunmpt  43963  sge0seq  43991  ovnsubaddlem1  44115  ovnsubaddlem2  44116  hoidmvlelem3  44142  hoidmvlelem4  44143  rrnmbl  44159  hoiqssbllem3  44169  hspmbl  44174  hoimbl  44176  issmflem  44272  issmfd  44280  issmfdf  44282  smfpimltmpt  44291  issmfled  44302  smfpimltxrmptf  44303  smfmbfcex  44305  issmfgtd  44306  smflimlem1  44316  smflimlem2  44317  smflimlem3  44318  smflimlem6  44321  smfpimgtmpt  44326  smfpimgtxrmptf  44329  smfres  44335  smfpimcclem  44351  smfpimcc  44352  dfateq12d  44629  ismgmd  45341  iscllaw  45394  islininds  45798  funcf2lem  46310  isthincd2lem2  46328