Theorem eleq12d 2832

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729  df-clel 2816

This theorem is referenced by:  neleq12d  3050  cbvraldva2  3367  cbvrexdva2  3368  cdeqel  3689  ru  3693  sbceqbid  3701  cbvrabcsfw  3855  cbvralcsf  3856  cbvreucsf  3858  cbvrabcsf  3859  sbcel12  4323  elvvuni  5625  elrnmpt1  5827  canth  7167  onnseq  8081  smoeq  8087  smores  8089  smores2  8091  iordsmo  8094  tz7.49  8181  nnaordr  8348  omsmolem  8382  fvixp  8583  cbvixp  8595  mptelixpg  8616  boxcutc  8622  ixpiunwdom  9206  elirr  9213  cantnflt  9287  oemapvali  9299  cantnflem1  9304  cantnf  9308  wemapwe  9312  cnfcom3lem  9318  infxpen  9628  dfac8alem  9643  dfac8clem  9646  ac5num  9650  acni2  9660  numacn  9663  acndom  9665  aceq3lem  9734  dfac5  9742  dfac9  9750  dfac13  9756  fin2i  9909  isfin2-2  9933  fin23lem27  9942  isfin3ds  9943  fin23lem17  9952  fin23lem39  9964  isf33lem  9980  isf34lem7  9993  isf34lem6  9994  fin1a2lem10  10023  fin1a2lem12  10025  hsmexlem4  10043  axcc2lem  10050  axcc3  10052  domtriomlem  10056  axdc2lem  10062  axdc3lem2  10065  axdc3lem3  10066  axdc3lem4  10067  axdc3  10068  axdc4lem  10069  axcclem  10071  ac6num  10093  ac6c4  10095  iundom2g  10154  fpwwe2  10257  pwfseqlem1  10272  pwfseqlem4a  10275  pwfseqlem4  10276  ltapi  10517  ltmpi  10518  eluzadd  12469  fzsubel  13148  elfzp1b  13189  axdc4uzlem  13556  wrd2ind  14288  smuval  16040  prdsbasprj  16977  xpsfrnel  17067  ismri2dad  17140  mreexd  17145  mreacs  17161  iscat  17175  iscatd  17176  iscatd2  17184  catcocl  17188  catpropd  17212  brssc  17319  issubc  17341  subcidcl  17350  subccocl  17351  isfunc  17370  isfuncd  17371  cofucl  17394  funcres2b  17403  fuciso  17484  yonedalem3  17788  yonffthlem  17790  ismgm  18115  issstrmgm  18125  ismndd  18195  eqgfval  18592  efgsdm  19120  efgsdmi  19122  efgsrel  19124  efgsp1  19127  efgsres  19128  dprdfcl  19400  ablfaclem3  19474  isdrngd  19792  issrng  19886  issrngd  19897  islmodd  19905  islbs  20113  lbsind  20117  lbspropd  20136  islbs2  20191  lbsextlem4  20198  lbsextg  20199  zndvds  20514  isphl  20590  isphld  20616  phlpropd  20617  frlmlbs  20759  islindf  20774  islinds2  20775  lindfind  20778  lindsind  20779  lindsind2  20781  lindfrn  20783  lindfmm  20789  lsslindf  20792  mhppwdeg  21090  mat1dimmul  21373  istps  21831  tpspropd  21835  eltpsg  21840  islp  22037  1stcelcls  22358  kgeni  22434  kgencn2  22454  ptpjpre1  22468  elptr2  22471  ptbasin  22474  ptbasfi  22478  ptpjcn  22508  ptpjopn  22509  ptcld  22510  ptcldmpt  22511  ptclsg  22512  ptcnp  22519  qtopval  22592  ptcmplem2  22950  ptcmplem3  22951  ptcmplem4  22952  istmd  22971  istgp  22974  tmdgsum  22992  istlm  23082  isusp  23159  prdsdsf  23265  prdsxmet  23267  isms  23347  mspropd  23372  setsxms  23377  setsms  23378  tmsxms  23384  tmsms  23385  isnrg  23558  tngnrg  23572  bcthlem2  24222  bcthlem3  24223  bcthlem4  24224  bcthlem5  24225  iscms  24242  cmspropd  24246  cmssmscld  24247  cmsss  24248  shft2rab  24405  ovolicc2lem3  24416  ovolicc2lem4  24417  ovolicc2lem5  24418  vitalilem2  24506  vitalilem3  24507  vitali  24510  limcfval  24769  limcmpt2  24781  limcres  24783  cnplimc  24784  cnlimci  24786  elcpn  24831  uc1pval  25037  ig1pcl  25073  jensen  25871  axtgcont  26560  tglngval  26642  ishlg  26693  mirbtwnb  26763  trgcopy  26895  trgcopyeu  26897  acopyeu  26925  isinagd  26930  tgasa1  26949  wlkp1lem3  27763  umgrwwlks2on  28041  clwwlknon1  28180  clwwlknonclwlknonf1o  28445  imsmet  28772  smcn  28779  iscbn  28945  sbceqbidf  30554  fnpreimac  30728  isslmd  31174  0nellinds  31280  lindssn  31287  lindfpropd  31290  elrspunidl  31320  lbslsat  31413  lindsunlem  31419  brfldext  31436  submateq  31473  lmatcl  31480  ispcmp  31521  zarcmplem  31545  zhmnrg  31629  ismntoplly  31687  sigapildsys  31842  fiunelcarsg  31995  eulerpartlemgvv  32055  eulerpart  32061  ptpconn  32908  cvmscbv  32933  cvmshmeo  32946  cvmsss2  32949  cvmliftlem7  32966  cvmliftlem10  32969  cvmlift2lem11  32988  cvmlift2lem12  32989  satffunlem1lem1  33077  satffunlem2lem1  33079  sategoelfvb  33094  prv1n  33106  elmpps  33248  ttrcltr  33515  rnttrcl  33521  naddel2  33577  bj-elabd2ALT  34850  currysetlem  34871  currysetlem1  34873  bj-ismoore  35011  csbfinxpg  35296  pibt2  35325  lindsadd  35507  lindsenlbs  35509  ptrest  35513  upixp  35624  sdclem1  35638  sstotbnd2  35669  prdsbnd2  35690  isprrngo  35945  isopos  36931  isatl  37050  isnacs3  40235  nacsfix  40237  mzpclall  40252  dnnumch1  40572  dnwech  40576  aomclem3  40584  aomclem8  40589  dfac11  40590  islmodfg  40597  rfovcnvf1od  41289  ismnu  41552  sblpnf  41601  rusbcALT  41730  choicefi  42413  climsuselem1  42823  climsuse  42824  cncfuni  43102  dvnprodlem1  43162  stoweidlem31  43247  stoweidlem59  43275  fourierdlem46  43368  fourierdlem62  43384  fourierdlem72  43394  fourierdlem79  43401  fourierdlem88  43410  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem112  43434  qndenserrnbllem  43510  ioorrnopnlem  43520  ioorrnopn  43521  ioorrnopnxr  43523  issal  43530  subsaliuncllem  43571  subsaliuncl  43572  subsalsal  43573  sge0tsms  43593  sge0iunmpt  43631  sge0seq  43659  ovnsubaddlem1  43783  ovnsubaddlem2  43784  hoidmvlelem3  43810  hoidmvlelem4  43811  rrnmbl  43827  hoiqssbllem3  43837  hspmbl  43842  hoimbl  43844  issmflem  43935  issmfd  43943  issmfdf  43945  smfpimltmpt  43954  issmfled  43965  smfpimltxrmpt  43966  smfmbfcex  43967  issmfgtd  43968  smflimlem1  43978  smflimlem2  43979  smflimlem3  43980  smflimlem6  43983  smfpimgtmpt  43988  smfpimgtxrmpt  43991  smfres  43996  smfpimcclem  44012  smfpimcc  44013  dfateq12d  44290  ismgmd  45003  iscllaw  45056  islininds  45460  funcf2lem  45972  isthincd2lem2  45990