Theorem eleq12d 2875

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1520   ∈ wcel 2079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760  df-cleq 2786  df-clel 2861

This theorem is referenced by:  neleq12d  3092  cbvraldva2  3404  cbvrexdva2  3405  cbvrexdva2OLD  3406  cdeqel  3696  ru  3700  sbceqbid  3708  cbvralcsf  3844  cbvreucsf  3846  cbvrabcsf  3847  sbcel12  4274  elvvuni  5506  elrnmpt1  5704  canth  6965  onnseq  7824  smoeq  7830  smores  7832  smores2  7834  iordsmo  7837  tz7.49  7923  nnaordr  8087  omsmolem  8121  fvixp  8305  cbvixp  8317  mptelixpg  8337  boxcutc  8343  ixpiunwdom  8891  elirr  8897  cantnflt  8970  oemapvali  8982  cantnflem1  8987  cantnf  8991  wemapwe  8995  cnfcom3lem  9001  infxpen  9275  dfac8alem  9290  dfac8clem  9293  ac5num  9297  acni2  9307  numacn  9310  acndom  9312  aceq3lem  9381  dfac5  9389  dfac9  9397  dfac13  9403  fin2i  9552  isfin2-2  9576  fin23lem27  9585  isfin3ds  9586  fin23lem17  9595  fin23lem39  9607  isf33lem  9623  isf34lem7  9636  isf34lem6  9637  fin1a2lem10  9666  fin1a2lem12  9668  hsmexlem4  9686  axcc2lem  9693  axcc3  9695  domtriomlem  9699  axdc2lem  9705  axdc3lem2  9708  axdc3lem3  9709  axdc3lem4  9710  axdc3  9711  axdc4lem  9712  axcclem  9714  ac6num  9736  ac6c4  9738  iundom2g  9797  fpwwe2  9900  pwfseqlem1  9915  pwfseqlem4a  9918  pwfseqlem4  9919  ltapi  10160  ltmpi  10161  eluzadd  12111  fzsubel  12782  elfzp1b  12823  axdc4uzlem  13189  wrd2ind  13909  smuval  15651  prdsbasprj  16562  xpsfrnel  16652  ismri2dad  16725  mreexd  16730  mreacs  16746  iscat  16760  iscatd  16761  iscatd2  16769  catcocl  16773  catpropd  16796  brssc  16901  issubc  16922  subcidcl  16931  subccocl  16932  isfunc  16951  isfuncd  16952  cofucl  16975  funcres2b  16984  fuciso  17062  yonedalem3  17347  yonffthlem  17349  ismgm  17670  issstrmgm  17679  ismndd  17740  eqgfval  18069  efgsdm  18571  efgsdmi  18573  efgsrel  18575  efgsp1  18578  efgsres  18579  dprdfcl  18840  ablfaclem3  18914  isdrngd  19205  issrng  19299  issrngd  19310  islmodd  19318  islbs  19526  lbsind  19530  lbspropd  19549  islbs2  19604  lbsextlem4  19611  lbsextg  19612  zndvds  20366  isphl  20442  isphld  20468  phlpropd  20469  frlmlbs  20611  islindf  20626  islinds2  20627  lindfind  20630  lindsind  20631  lindsind2  20633  lindfrn  20635  lindfmm  20641  lsslindf  20644  mat1dimmul  20757  istps  21214  tpspropd  21218  eltpsg  21223  islp  21420  1stcelcls  21741  kgeni  21817  kgencn2  21837  ptpjpre1  21851  elptr2  21854  ptbasin  21857  ptbasfi  21861  ptpjcn  21891  ptpjopn  21892  ptcld  21893  ptcldmpt  21894  ptclsg  21895  ptcnp  21902  qtopval  21975  ptcmplem2  22333  ptcmplem3  22334  ptcmplem4  22335  istmd  22354  istgp  22357  tmdgsum  22375  istlm  22464  isusp  22541  prdsdsf  22648  prdsxmet  22650  isms  22730  mspropd  22755  setsxms  22760  setsms  22761  tmsxms  22767  tmsms  22768  isnrg  22940  tngnrg  22954  bcthlem2  23599  bcthlem3  23600  bcthlem4  23601  bcthlem5  23602  iscms  23619  cmspropd  23623  cmssmscld  23624  cmsss  23625  shft2rab  23780  ovolicc2lem3  23791  ovolicc2lem4  23792  ovolicc2lem5  23793  vitalilem2  23881  vitalilem3  23882  vitali  23885  limcfval  24141  limcmpt2  24153  limcres  24155  cnplimc  24156  cnlimci  24158  elcpn  24202  uc1pval  24404  ig1pcl  24440  jensen  25236  axtgcont  25925  tglngval  26007  ishlg  26058  mirbtwnb  26128  trgcopy  26260  trgcopyeu  26262  acopyeu  26291  isinagd  26296  tgasa1  26315  wlkp1lem3  27130  umgrwwlks2on  27411  clwwlknon1  27551  clwwlknonclwlknonf1o  27821  imsmet  28147  smcn  28154  iscbn  28320  sbceqbidf  29929  fnpreimac  30079  isslmd  30426  0nellinds  30538  lindssn  30540  lindfpropd  30543  lbslsat  30573  lindsunlem  30579  brfldext  30596  submateq  30645  lmatcl  30652  ispcmp  30694  zhmnrg  30781  ismntoplly  30839  inelpisys  30986  sigapildsys  30994  fiunelcarsg  31147  eulerpartlemgvv  31207  eulerpart  31213  ptpconn  32044  cvmscbv  32069  cvmshmeo  32082  cvmsss2  32085  cvmliftlem7  32102  cvmliftlem10  32105  cvmlift2lem11  32124  cvmlift2lem12  32125  satffunlem1lem1  32210  satffunlem2lem1  32212  sategoelfvb  32227  elmpps  32373  currysetlem  33773  currysetlem1  33775  bj-ismoore  33942  csbfinxpg  34146  pibt2  34175  lindsadd  34362  lindsenlbs  34364  ptrest  34368  upixp  34482  sdclem1  34496  sstotbnd2  34530  prdsbnd2  34551  isprrngo  34806  isopos  35797  isatl  35916  isnacs3  38742  nacsfix  38744  mzpclall  38759  dnnumch1  39080  dnwech  39084  aomclem3  39092  aomclem8  39097  dfac11  39098  islmodfg  39105  rfovcnvf1od  39786  ismnu  40046  sblpnf  40132  rusbcALT  40261  choicefi  40956  climsuselem1  41384  climsuse  41385  cncfuni  41664  dvnprodlem1  41726  stoweidlem31  41812  stoweidlem59  41840  fourierdlem46  41933  fourierdlem62  41949  fourierdlem72  41959  fourierdlem79  41966  fourierdlem88  41975  fourierdlem89  41976  fourierdlem90  41977  fourierdlem91  41978  fourierdlem112  41999  qndenserrnbllem  42075  ioorrnopnlem  42085  ioorrnopn  42086  ioorrnopnxr  42088  issal  42095  subsaliuncllem  42136  subsaliuncl  42137  subsalsal  42138  sge0tsms  42158  sge0iunmpt  42196  sge0seq  42224  ovnsubaddlem1  42348  ovnsubaddlem2  42349  hoidmvlelem3  42375  hoidmvlelem4  42376  rrnmbl  42392  hoiqssbllem3  42402  hspmbl  42407  hoimbl  42409  issmflem  42500  issmfd  42508  issmfdf  42510  smfpimltmpt  42519  issmfled  42530  smfpimltxrmpt  42531  smfmbfcex  42532  issmfgtd  42533  smflimlem1  42543  smflimlem2  42544  smflimlem3  42545  smflimlem6  42548  smfpimgtmpt  42553  smfpimgtxrmpt  42556  smfres  42561  smfco  42573  smfpimcclem  42577  smfpimcc  42578  dfateq12d  42795  ismgmd  43479  iscllaw  43528  islininds  43935