Theorem eleq12d 2855

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  neleq12d  3065  cbvraldva2  3337  cdeqel  3737  sbceqbid  3749  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  sbcel12  4362  elvvuni  5720  elrnmpt1  5932  canth  7344  onnseq  8308  smoeq  8314  smores  8316  smores2  8318  iordsmo  8321  tz7.49  8409  nnaordr  8583  omsmolem  8620  naddel2  8652  fvixp  8877  cbvixp  8889  cbvixpv  8890  mptelixpg  8910  boxcutc  8916  ixpiunwdom  9531  elirr  9541  cantnflt  9620  oemapvali  9632  cantnflem1  9637  cantnf  9641  wemapwe  9645  cnfcom3lem  9651  ttrcltr  9664  rnttrcl  9670  infxpen  9963  dfac8alem  9978  dfac8clem  9981  ac5num  9985  acni2  9995  numacn  9998  acndom  10000  aceq3lem  10069  dfac5  10078  dfac9  10086  dfac13  10092  fin2i  10245  isfin2-2  10269  fin23lem27  10278  isfin3ds  10279  fin23lem17  10288  fin23lem39  10300  isf33lem  10316  isf34lem7  10329  isf34lem6  10330  fin1a2lem10  10359  fin1a2lem12  10361  hsmexlem4  10379  axcc2lem  10386  axcc3  10388  domtriomlem  10392  axdc2lem  10398  axdc3lem2  10401  axdc3lem3  10402  axdc3lem4  10403  axdc3  10404  axdc4lem  10405  axcclem  10407  ac6num  10429  ac6c4  10431  iundom2g  10490  fpwwe2  10594  pwfseqlem1  10609  pwfseqlem4a  10612  pwfseqlem4  10613  ltapi  10854  ltmpi  10855  fzsubel  13558  elfzp1b  13599  axdc4uzlem  13989  wrd2ind  14729  smuval  16505  prdsbasprj  17491  xpsfrnel  17582  ismri2dad  17659  mreexd  17664  mreacs  17680  iscat  17694  iscatd  17695  iscatd2  17703  catcocl  17707  catpropd  17731  brssc  17837  issubc  17858  subcidcl  17867  subccocl  17868  isfunc  17887  isfuncd  17888  cofucl  17911  funcres2b  17920  fuciso  18001  yonedalem3  18302  yonffthlem  18304  ismgm  18665  ismgmd  18676  issstrmgm  18677  issgrpd  18754  ismndd  18780  eqgfval  19207  efgsdm  19760  efgsdmi  19762  efgsrel  19764  efgsp1  19767  efgsres  19768  dprdfcl  20045  ablfaclem3  20119  isdrngd  20801  isdrngdOLD  20803  issrng  20880  issrngd  20891  islmodd  20920  islbs  21130  lbsind  21134  lbspropd  21153  islbs2  21211  lbsextlem4  21218  lbsextg  21219  pzriprnglem8  21527  zndvds  21588  isphl  21667  isphld  21693  phlpropd  21694  frlmlbs  21836  islindf  21851  islinds2  21852  lindfind  21855  lindsind  21856  lindsind2  21858  lindfrn  21860  lindfmm  21866  lsslindf  21869  mhppwdeg  22202  mat1dimmul  22523  istps  22981  tpspropd  22985  eltpsg  22990  islp  23187  1stcelcls  23508  kgeni  23584  kgencn2  23604  ptpjpre1  23618  elptr2  23621  ptbasin  23624  ptbasfi  23628  ptpjcn  23658  ptpjopn  23659  ptcld  23660  ptcldmpt  23661  ptclsg  23662  ptcnp  23669  qtopval  23742  ptcmplem2  24100  ptcmplem3  24101  ptcmplem4  24102  istmd  24121  istgp  24124  tmdgsum  24142  istlm  24232  isusp  24308  prdsdsf  24414  prdsxmet  24416  isms  24496  mspropd  24521  setsxms  24526  setsms  24527  tmsxms  24533  tmsms  24534  isnrg  24707  tngnrg  24721  bcthlem2  25374  bcthlem3  25375  bcthlem4  25376  bcthlem5  25377  iscms  25394  cmspropd  25398  cmssmscld  25399  cmsss  25400  shft2rab  25557  ovolicc2lem3  25568  ovolicc2lem4  25569  ovolicc2lem5  25570  vitalilem2  25658  vitalilem3  25659  vitali  25662  limcfval  25921  limcmpt2  25933  limcres  25935  cnplimc  25936  cnlimci  25938  elcpn  25983  uc1pval  26187  ig1pcl  26226  jensen  27040  axtgcont  28625  tglngval  28707  ishlg  28758  mirbtwnb  28828  trgcopy  28960  trgcopyeu  28962  acopyeu  28990  isinagd  28995  tgasa1  29014  wlkp1lem3  29830  usgrwwlks2on  30114  umgrwwlks2on  30115  clwwlknon1  30255  clwwlknonclwlknonf1o  30520  imsmet  30850  smcn  30857  iscbn  31023  sbceqbidf  32644  fnpreimac  32832  isslmd  33342  0nellinds  33516  lindssn  33524  lindfpropd  33528  elrspunidl  33574  lbslsat  33873  lindsunlem  33881  brfldext  33902  submateq  34066  lmatcl  34073  ispcmp  34114  zarcmplem  34138  zhmnrg  34222  ismntoplly  34282  sigapildsys  34419  fiunelcarsg  34573  eulerpartlemgvv  34633  eulerpart  34639  fineqvinfep  35381  onvf1odlem2  35407  ptpconn  35543  cvmscbv  35568  cvmshmeo  35581  cvmsss2  35584  cvmliftlem7  35601  cvmliftlem10  35604  cvmlift2lem11  35623  cvmlift2lem12  35624  satffunlem1lem1  35712  satffunlem2lem1  35714  sategoelfvb  35729  prv1n  35741  elmpps  35883  nmulprop  36500  nmulcom  36504  cbvriotavw2  36556  cbvmpovw2  36562  cbvmpo1vw2  36563  cbvmpo2vw2  36564  cbvixpvw2  36565  cbvitgvw2  36568  cbvsbcdavw2  36578  cbvixpdavw  36598  cbvrmodavw2  36603  cbvreudavw2  36604  cbvmpodavw2  36611  cbvmpo1davw2  36612  cbvmpo2davw2  36613  cbvixpdavw2  36614  cbvproddavw2  36616  cbvitgdavw2  36617  weiunpo  36785  weiunso  36786  weiunfr  36787  weiunse  36788  bj-elabd2ALT  37370  bj-ru1  37388  currysetlem  37390  currysetlem1  37392  bj-ismoore  37555  csbfinxpg  37842  pibt2  37871  lindsadd  38072  lindsenlbs  38074  ptrest  38078  upixp  38188  sdclem1  38202  sstotbnd2  38233  prdsbnd2  38254  isprrngo  38509  isopos  39764  isatl  39883  aks6d1c1p6  42691  isnacs3  43251  nacsfix  43253  mzpclall  43268  dnnumch1  43581  dnwech  43585  aomclem3  43593  aomclem8  43598  dfac11  43599  islmodfg  43606  oaordnr  43833  omnord1  43842  oenord1  43853  cantnfresb  43861  rfovcnvf1od  44540  ismnu  44797  sblpnf  44846  rusbcALT  44974  cbvrabv2w  45666  choicefi  45737  climsuselem1  46143  climsuse  46144  cncfuni  46420  dvnprodlem1  46480  stoweidlem31  46565  stoweidlem59  46593  fourierdlem46  46686  fourierdlem62  46702  fourierdlem72  46712  fourierdlem79  46719  fourierdlem88  46728  fourierdlem89  46729  fourierdlem90  46730  fourierdlem91  46731  fourierdlem112  46752  qndenserrnbllem  46828  ioorrnopnlem  46838  ioorrnopn  46839  ioorrnopnxr  46841  issal  46848  subsaliuncllem  46891  subsaliuncl  46892  subsalsal  46893  sge0tsms  46914  sge0iunmpt  46952  sge0seq  46980  ovnsubaddlem1  47104  ovnsubaddlem2  47105  hoidmvlelem3  47131  hoidmvlelem4  47132  rrnmbl  47148  hoiqssbllem3  47158  hspmbl  47163  hoimbl  47165  issmflem  47261  issmfd  47269  issmfdf  47271  smfpimltmpt  47280  issmfled  47291  smfpimltxrmptf  47292  smfmbfcex  47294  issmfgtd  47295  smflimlem1  47305  smflimlem2  47306  smflimlem3  47307  smflimlem6  47310  smfpimgtmpt  47315  smfpimgtxrmptf  47318  smfres  47324  smfpimcclem  47341  smfpimcc  47342  dfateq12d  47680  iscllaw  48771  islininds  49028  brab2ddw  49410  brab2ddw2  49411  funcf2lem  49662  isthincd2lem2  50016  setc1onsubc  50183