Theorem eleq12d 2830

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

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

This theorem is referenced by:  neleq12d  3041  cbvraldva2  3313  cdeqel  3722  ruOLD  3727  sbceqbid  3735  cbvrabcsfw  3878  cbvralcsf  3879  cbvreucsf  3881  cbvrabcsf  3882  sbcel12  4351  elvvuni  5708  elrnmpt1  5915  canth  7321  onnseq  8284  smoeq  8290  smores  8292  smores2  8294  iordsmo  8297  tz7.49  8384  nnaordr  8556  omsmolem  8593  naddel2  8624  fvixp  8850  cbvixp  8862  cbvixpv  8863  mptelixpg  8883  boxcutc  8889  ixpiunwdom  9505  elirr  9514  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  13514  elfzp1b  13555  axdc4uzlem  13945  wrd2ind  14685  smuval  16450  prdsbasprj  17435  xpsfrnel  17526  ismri2dad  17603  mreexd  17608  mreacs  17624  iscat  17638  iscatd  17639  iscatd2  17647  catcocl  17651  catpropd  17675  brssc  17781  issubc  17802  subcidcl  17811  subccocl  17812  isfunc  17831  isfuncd  17832  cofucl  17855  funcres2b  17864  fuciso  17945  yonedalem3  18246  yonffthlem  18248  ismgm  18609  ismgmd  18620  issstrmgm  18621  issgrpd  18698  ismndd  18724  eqgfval  19151  efgsdm  19705  efgsdmi  19707  efgsrel  19709  efgsp1  19712  efgsres  19713  dprdfcl  19990  ablfaclem3  20064  isdrngd  20742  isdrngdOLD  20744  issrng  20821  issrngd  20832  islmodd  20861  islbs  21071  lbsind  21075  lbspropd  21094  islbs2  21152  lbsextlem4  21159  lbsextg  21160  pzriprnglem8  21468  zndvds  21529  isphl  21608  isphld  21634  phlpropd  21635  frlmlbs  21777  islindf  21792  islinds2  21793  lindfind  21796  lindsind  21797  lindsind2  21799  lindfrn  21801  lindfmm  21807  lsslindf  21810  mhppwdeg  22116  mat1dimmul  22441  istps  22899  tpspropd  22903  eltpsg  22908  islp  23105  1stcelcls  23426  kgeni  23502  kgencn2  23522  ptpjpre1  23536  elptr2  23539  ptbasin  23542  ptbasfi  23546  ptpjcn  23576  ptpjopn  23577  ptcld  23578  ptcldmpt  23579  ptclsg  23580  ptcnp  23587  qtopval  23660  ptcmplem2  24018  ptcmplem3  24019  ptcmplem4  24020  istmd  24039  istgp  24042  tmdgsum  24060  istlm  24150  isusp  24226  prdsdsf  24332  prdsxmet  24334  isms  24414  mspropd  24439  setsxms  24444  setsms  24445  tmsxms  24451  tmsms  24452  isnrg  24625  tngnrg  24639  bcthlem2  25292  bcthlem3  25293  bcthlem4  25294  bcthlem5  25295  iscms  25312  cmspropd  25316  cmssmscld  25317  cmsss  25318  shft2rab  25475  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2lem5  25488  vitalilem2  25576  vitalilem3  25577  vitali  25580  limcfval  25839  limcmpt2  25851  limcres  25853  cnplimc  25854  cnlimci  25856  elcpn  25901  uc1pval  26105  ig1pcl  26144  jensen  26952  axtgcont  28537  tglngval  28619  ishlg  28670  mirbtwnb  28740  trgcopy  28872  trgcopyeu  28874  acopyeu  28902  isinagd  28907  tgasa1  28926  wlkp1lem3  29742  usgrwwlks2on  30026  umgrwwlks2on  30027  clwwlknon1  30167  clwwlknonclwlknonf1o  30432  imsmet  30762  smcn  30769  iscbn  30935  sbceqbidf  32556  fnpreimac  32743  isslmd  33263  0nellinds  33430  lindssn  33438  lindfpropd  33442  elrspunidl  33488  lbslsat  33760  lindsunlem  33768  brfldext  33789  submateq  33953  lmatcl  33960  ispcmp  34001  zarcmplem  34025  zhmnrg  34109  ismntoplly  34169  sigapildsys  34306  fiunelcarsg  34460  eulerpartlemgvv  34520  eulerpart  34526  fineqvinfep  35269  onvf1odlem2  35286  ptpconn  35415  cvmscbv  35440  cvmshmeo  35453  cvmsss2  35456  cvmliftlem7  35473  cvmliftlem10  35476  cvmlift2lem11  35495  cvmlift2lem12  35496  satffunlem1lem1  35584  satffunlem2lem1  35586  sategoelfvb  35601  prv1n  35613  elmpps  35755  cbvriotavw2  36418  cbvmpovw2  36424  cbvmpo1vw2  36425  cbvmpo2vw2  36426  cbvixpvw2  36427  cbvitgvw2  36430  cbvsbcdavw2  36440  cbvixpdavw  36460  cbvrmodavw2  36465  cbvreudavw2  36466  cbvmpodavw2  36473  cbvmpo1davw2  36474  cbvmpo2davw2  36475  cbvixpdavw2  36476  cbvproddavw2  36478  cbvitgdavw2  36479  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  bj-elabd2ALT  37232  bj-ru1  37250  currysetlem  37252  currysetlem1  37254  bj-ismoore  37417  csbfinxpg  37704  pibt2  37733  lindsadd  37934  lindsenlbs  37936  ptrest  37940  upixp  38050  sdclem1  38064  sstotbnd2  38095  prdsbnd2  38116  isprrngo  38371  isopos  39626  isatl  39745  aks6d1c1p6  42553  isnacs3  43142  nacsfix  43144  mzpclall  43159  dnnumch1  43472  dnwech  43476  aomclem3  43484  aomclem8  43489  dfac11  43490  islmodfg  43497  oaordnr  43724  omnord1  43733  oenord1  43744  cantnfresb  43752  rfovcnvf1od  44431  ismnu  44688  sblpnf  44737  rusbcALT  44865  cbvrabv2w  45558  choicefi  45629  climsuselem1  46037  climsuse  46038  cncfuni  46314  dvnprodlem1  46374  stoweidlem31  46459  stoweidlem59  46487  fourierdlem46  46580  fourierdlem62  46596  fourierdlem72  46606  fourierdlem79  46613  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem112  46646  qndenserrnbllem  46722  ioorrnopnlem  46732  ioorrnopn  46733  ioorrnopnxr  46735  issal  46742  subsaliuncllem  46785  subsaliuncl  46786  subsalsal  46787  sge0tsms  46808  sge0iunmpt  46846  sge0seq  46874  ovnsubaddlem1  46998  ovnsubaddlem2  46999  hoidmvlelem3  47025  hoidmvlelem4  47026  rrnmbl  47042  hoiqssbllem3  47052  hspmbl  47057  hoimbl  47059  issmflem  47155  issmfd  47163  issmfdf  47165  smfpimltmpt  47174  issmfled  47185  smfpimltxrmptf  47186  smfmbfcex  47188  issmfgtd  47189  smflimlem1  47199  smflimlem2  47200  smflimlem3  47201  smflimlem6  47204  smfpimgtmpt  47209  smfpimgtxrmptf  47212  smfres  47218  smfpimcclem  47235  smfpimcc  47236  dfateq12d  47574  iscllaw  48665  islininds  48922  brab2ddw  49304  brab2ddw2  49305  funcf2lem  49556  isthincd2lem2  49910  setc1onsubc  50077