Theorem eleq12d 2831

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 279	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  neleq12d  3042  cbvraldva2  3320  cdeqel  3736  ruOLD  3741  sbceqbid  3749  cbvrabcsfw  3892  cbvralcsf  3893  cbvreucsf  3895  cbvrabcsf  3896  sbcel12  4365  elvvuni  5709  elrnmpt1  5917  canth  7322  onnseq  8286  smoeq  8292  smores  8294  smores2  8296  iordsmo  8299  tz7.49  8386  nnaordr  8558  omsmolem  8595  naddel2  8626  fvixp  8852  cbvixp  8864  cbvixpv  8865  mptelixpg  8885  boxcutc  8891  ixpiunwdom  9507  elirr  9516  cantnflt  9593  oemapvali  9605  cantnflem1  9610  cantnf  9614  wemapwe  9618  cnfcom3lem  9624  ttrcltr  9637  rnttrcl  9643  infxpen  9936  dfac8alem  9951  dfac8clem  9954  ac5num  9958  acni2  9968  numacn  9971  acndom  9973  aceq3lem  10042  dfac5  10051  dfac9  10059  dfac13  10065  fin2i  10217  isfin2-2  10241  fin23lem27  10250  isfin3ds  10251  fin23lem17  10260  fin23lem39  10272  isf33lem  10288  isf34lem7  10301  isf34lem6  10302  fin1a2lem10  10331  fin1a2lem12  10333  hsmexlem4  10351  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3lem4  10375  axdc3  10376  axdc4lem  10377  axcclem  10379  ac6num  10401  ac6c4  10403  iundom2g  10462  fpwwe2  10566  pwfseqlem1  10581  pwfseqlem4a  10584  pwfseqlem4  10585  ltapi  10826  ltmpi  10827  fzsubel  13488  elfzp1b  13529  axdc4uzlem  13918  wrd2ind  14658  smuval  16420  prdsbasprj  17404  xpsfrnel  17495  ismri2dad  17572  mreexd  17577  mreacs  17593  iscat  17607  iscatd  17608  iscatd2  17616  catcocl  17620  catpropd  17644  brssc  17750  issubc  17771  subcidcl  17780  subccocl  17781  isfunc  17800  isfuncd  17801  cofucl  17824  funcres2b  17833  fuciso  17914  yonedalem3  18215  yonffthlem  18217  ismgm  18578  ismgmd  18589  issstrmgm  18590  issgrpd  18667  ismndd  18693  eqgfval  19117  efgsdm  19671  efgsdmi  19673  efgsrel  19675  efgsp1  19678  efgsres  19679  dprdfcl  19956  ablfaclem3  20030  isdrngd  20710  isdrngdOLD  20712  issrng  20789  issrngd  20800  islmodd  20829  islbs  21040  lbsind  21044  lbspropd  21063  islbs2  21121  lbsextlem4  21128  lbsextg  21129  pzriprnglem8  21455  zndvds  21516  isphl  21595  isphld  21621  phlpropd  21622  frlmlbs  21764  islindf  21779  islinds2  21780  lindfind  21783  lindsind  21784  lindsind2  21786  lindfrn  21788  lindfmm  21794  lsslindf  21797  mhppwdeg  22105  mat1dimmul  22432  istps  22890  tpspropd  22894  eltpsg  22899  islp  23096  1stcelcls  23417  kgeni  23493  kgencn2  23513  ptpjpre1  23527  elptr2  23530  ptbasin  23533  ptbasfi  23537  ptpjcn  23567  ptpjopn  23568  ptcld  23569  ptcldmpt  23570  ptclsg  23571  ptcnp  23578  qtopval  23651  ptcmplem2  24009  ptcmplem3  24010  ptcmplem4  24011  istmd  24030  istgp  24033  tmdgsum  24051  istlm  24141  isusp  24217  prdsdsf  24323  prdsxmet  24325  isms  24405  mspropd  24430  setsxms  24435  setsms  24436  tmsxms  24442  tmsms  24443  isnrg  24616  tngnrg  24630  bcthlem2  25293  bcthlem3  25294  bcthlem4  25295  bcthlem5  25296  iscms  25313  cmspropd  25317  cmssmscld  25318  cmsss  25319  shft2rab  25477  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2lem5  25490  vitalilem2  25578  vitalilem3  25579  vitali  25582  limcfval  25841  limcmpt2  25853  limcres  25855  cnplimc  25856  cnlimci  25858  elcpn  25904  uc1pval  26113  ig1pcl  26152  jensen  26967  axtgcont  28553  tglngval  28635  ishlg  28686  mirbtwnb  28756  trgcopy  28888  trgcopyeu  28890  acopyeu  28918  isinagd  28923  tgasa1  28942  wlkp1lem3  29759  usgrwwlks2on  30043  umgrwwlks2on  30044  clwwlknon1  30184  clwwlknonclwlknonf1o  30449  imsmet  30778  smcn  30785  iscbn  30951  sbceqbidf  32572  fnpreimac  32759  isslmd  33295  0nellinds  33462  lindssn  33470  lindfpropd  33474  elrspunidl  33520  lbslsat  33793  lindsunlem  33801  brfldext  33822  submateq  33986  lmatcl  33993  ispcmp  34034  zarcmplem  34058  zhmnrg  34142  ismntoplly  34202  sigapildsys  34339  fiunelcarsg  34493  eulerpartlemgvv  34553  eulerpart  34559  fineqvinfep  35300  onvf1odlem2  35317  ptpconn  35446  cvmscbv  35471  cvmshmeo  35484  cvmsss2  35487  cvmliftlem7  35504  cvmliftlem10  35507  cvmlift2lem11  35526  cvmlift2lem12  35527  satffunlem1lem1  35615  satffunlem2lem1  35617  sategoelfvb  35632  prv1n  35644  elmpps  35786  cbvriotavw2  36449  cbvmpovw2  36455  cbvmpo1vw2  36456  cbvmpo2vw2  36457  cbvixpvw2  36458  cbvitgvw2  36461  cbvsbcdavw2  36471  cbvixpdavw  36491  cbvrmodavw2  36496  cbvreudavw2  36497  cbvmpodavw2  36504  cbvmpo1davw2  36505  cbvmpo2davw2  36506  cbvixpdavw2  36507  cbvproddavw2  36509  cbvitgdavw2  36510  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  bj-elabd2ALT  37170  bj-ru1  37188  currysetlem  37190  currysetlem1  37192  bj-ismoore  37355  csbfinxpg  37640  pibt2  37669  lindsadd  37861  lindsenlbs  37863  ptrest  37867  upixp  37977  sdclem1  37991  sstotbnd2  38022  prdsbnd2  38043  isprrngo  38298  isopos  39553  isatl  39672  aks6d1c1p6  42481  isnacs3  43064  nacsfix  43066  mzpclall  43081  dnnumch1  43398  dnwech  43402  aomclem3  43410  aomclem8  43415  dfac11  43416  islmodfg  43423  oaordnr  43650  omnord1  43659  oenord1  43670  cantnfresb  43678  rfovcnvf1od  44357  ismnu  44614  sblpnf  44663  rusbcALT  44791  cbvrabv2w  45484  choicefi  45555  climsuselem1  45964  climsuse  45965  cncfuni  46241  dvnprodlem1  46301  stoweidlem31  46386  stoweidlem59  46414  fourierdlem46  46507  fourierdlem62  46523  fourierdlem72  46533  fourierdlem79  46540  fourierdlem88  46549  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem112  46573  qndenserrnbllem  46649  ioorrnopnlem  46659  ioorrnopn  46660  ioorrnopnxr  46662  issal  46669  subsaliuncllem  46712  subsaliuncl  46713  subsalsal  46714  sge0tsms  46735  sge0iunmpt  46773  sge0seq  46801  ovnsubaddlem1  46925  ovnsubaddlem2  46926  hoidmvlelem3  46952  hoidmvlelem4  46953  rrnmbl  46969  hoiqssbllem3  46979  hspmbl  46984  hoimbl  46986  issmflem  47082  issmfd  47090  issmfdf  47092  smfpimltmpt  47101  issmfled  47112  smfpimltxrmptf  47113  smfmbfcex  47115  issmfgtd  47116  smflimlem1  47126  smflimlem2  47127  smflimlem3  47128  smflimlem6  47131  smfpimgtmpt  47136  smfpimgtxrmptf  47139  smfres  47145  smfpimcclem  47162  smfpimcc  47163  dfateq12d  47483  iscllaw  48546  islininds  48803  brab2ddw  49185  brab2ddw2  49186  funcf2lem  49437  isthincd2lem2  49791  setc1onsubc  49958