Theorem eleq12d 2682

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  neleq12d  2887  cbvraldva2  3151  cbvrexdva2  3152  cdeqel  3398  ru  3401  sbceqbid  3409  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbcel12  3935  elvvuni  5102  elrnmpt1  5295  canth  6508  onnseq  7328  smoeq  7334  smores  7336  smores2  7338  iordsmo  7341  tz7.49  7427  nnaordr  7587  omsmolem  7620  fvixp  7799  cbvixp  7811  mptelixpg  7831  boxcutc  7837  ixpiunwdom  8379  elirr  8388  cantnflt  8452  oemapvali  8464  cantnflem1  8469  cantnf  8473  wemapwe  8477  cnfcom3lem  8483  infxpen  8720  dfac8alem  8735  dfac8clem  8738  ac5num  8742  acni2  8752  numacn  8755  acndom  8757  aceq3lem  8826  dfac5  8834  dfac9  8841  dfac13  8847  fin2i  9000  isfin2-2  9024  fin23lem27  9033  isfin3ds  9034  fin23lem17  9043  fin23lem39  9055  isf33lem  9071  isf34lem7  9084  isf34lem6  9085  fin1a2lem10  9114  fin1a2lem12  9116  hsmexlem4  9134  axcc2lem  9141  axcc3  9143  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  axdc3lem3  9157  axdc3lem4  9158  axdc3  9159  axdc4lem  9160  axcclem  9162  ac6num  9184  ac6c4  9186  iundom2g  9241  fpwwe2  9344  pwfseqlem1  9359  pwfseqlem4a  9362  pwfseqlem4  9363  ltapi  9604  ltmpi  9605  eluzadd  11592  fzsubel  12248  elfzp1b  12286  axdc4uzlem  12644  wrd2ind  13329  smuval  15041  prdsbasprj  15955  xpsfrnel  16046  ismri2dad  16120  mreexd  16125  mreacs  16142  iscat  16156  iscatd  16157  iscatd2  16165  catcocl  16169  catpropd  16192  brssc  16297  issubc  16318  subcidcl  16327  subccocl  16328  isfunc  16347  isfuncd  16348  cofucl  16371  funcres2b  16380  fuciso  16458  yonedalem3  16743  yonffthlem  16745  ismgm  17066  issstrmgm  17075  ismndd  17136  eqgfval  17465  efgsdm  17966  efgsdmi  17968  efgsrel  17970  efgsp1  17973  efgsres  17974  dprdfcl  18235  ablfaclem3  18309  isdrngd  18595  issrng  18673  issrngd  18684  islmodd  18692  islbs  18897  lbsind  18901  lbspropd  18920  islbs2  18975  lbsextlem4  18982  lbsextg  18983  zndvds  19717  isphl  19792  isphld  19818  phlpropd  19819  frlmlbs  19955  islindf  19970  islinds2  19971  lindfind  19974  lindsind  19975  lindsind2  19977  lindfrn  19979  lindfmm  19985  lsslindf  19988  mat1dimmul  20101  istps  20551  tpspropd  20555  eltpsg  20560  islp  20754  1stcelcls  21074  kgeni  21150  kgencn2  21170  ptpjpre1  21184  elptr2  21187  ptbasin  21190  ptbasfi  21194  ptpjcn  21224  ptpjopn  21225  ptcld  21226  ptcldmpt  21227  ptclsg  21228  ptcnp  21235  qtopval  21308  ptcmplem2  21667  ptcmplem3  21668  ptcmplem4  21669  istmd  21688  istgp  21691  tmdgsum  21709  istlm  21798  isusp  21875  prdsdsf  21982  prdsxmet  21984  isms  22064  mspropd  22089  setsxms  22094  setsms  22095  tmsxms  22101  tmsms  22102  isnrg  22274  tngnrg  22288  bcthlem2  22930  bcthlem3  22931  bcthlem4  22932  bcthlem5  22933  iscms  22950  cmspropd  22954  cmsss  22955  shft2rab  23083  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  vitalilem2  23184  vitalilem3  23185  vitali  23188  limcfval  23442  limcmpt2  23454  limcres  23456  cnplimc  23457  cnlimci  23459  elcpn  23503  uc1pval  23703  ig1pcl  23739  jensen  24515  axtgcont  25168  tglngval  25246  ishlg  25297  mirbtwnb  25367  islnopp  25431  outpasch  25447  colhp  25462  trgcopy  25496  trgcopyeu  25498  dfcgra2  25521  acopyeu  25525  isinag  25529  tgasa1  25539  nbgraop  25952  nbgraopALT  25953  imsmet  26930  smcn  26937  iscbn  27104  sbceqbidf  28705  isslmd  29086  submateq  29203  lmatcl  29210  ispcmp  29252  zhmnrg  29339  ismntoplly  29397  inelpisys  29544  sigapildsys  29552  fiunelcarsg  29705  eulerpartlemgvv  29765  eulerpart  29771  ptpcon  30469  cvmscbv  30494  cvmshmeo  30507  cvmsss2  30510  cvmliftlem7  30527  cvmliftlem10  30530  cvmlift2lem11  30549  cvmlift2lem12  30550  elmpps  30724  csbfinxpg  32401  lindsenlbs  32574  ptrest  32578  upixp  32694  sdclem1  32709  sstotbnd2  32743  prdsbnd2  32764  isprrngo  33019  isopos  33485  isatl  33604  isnacs3  36291  nacsfix  36293  mzpclall  36308  dnnumch1  36632  dnwech  36636  aomclem3  36644  aomclem8  36649  dfac11  36650  islmodfg  36657  rfovcnvf1od  37318  sblpnf  37531  rusbcALT  37662  sbcel12gOLD  37775  choicefi  38387  climsuselem1  38674  climsuse  38675  cncfuni  38772  dvnprodlem1  38836  stoweidlem31  38924  stoweidlem59  38952  fourierdlem46  39045  fourierdlem62  39061  fourierdlem72  39071  fourierdlem79  39078  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem112  39111  qndenserrnbllem  39190  ioorrnopnlem  39200  ioorrnopn  39201  ioorrnopnxr  39203  issal  39210  subsaliuncllem  39251  subsaliuncl  39252  subsalsal  39253  sge0tsms  39273  sge0iunmpt  39311  sge0seq  39339  ovnsubaddlem1  39460  ovnsubaddlem2  39461  hoidmvlelem3  39487  hoidmvlelem4  39488  rrnmbl  39504  hoiqssbllem3  39514  hspmbl  39519  hoimbl  39521  issmflem  39613  issmfd  39621  issmfdf  39624  smfpimltmpt  39633  issmfled  39644  smfpimltxrmpt  39645  smfmbfcex  39646  issmfgtd  39647  smflimlem1  39657  smflimlem2  39658  smflimlem3  39659  smflimlem6  39662  smfpimgtmpt  39667  smfpimgtxrmpt  39670  smfres  39675  smfco  39687  dfateq12d  39858  1wlkp1lem3  40884  umgrwwlks2on  41161  ismgmd  41566  iscllaw  41615  islininds  42029