Theorem eleq12d 2859

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840

This theorem is used by:  neleq12d  3071  cbvraldva2  3342  cdeqel  3741  sbceqbid  3753  cbvrabcsfw  3895  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  sbcel12  4376  elvvuni  5740  elrnmpt1  5952  canth  7370  onnseq  8333  smoeq  8339  smores  8341  smores2  8343  iordsmo  8346  tz7.49  8434  nnaordr  8608  omsmolem  8645  naddel2  8677  fvixp  8902  cbvixp  8914  cbvixpv  8915  mptelixpg  8935  boxcutc  8941  ixpiunwdom  9555  elirr  9565  cantnflt  9644  oemapvali  9656  cantnflem1  9661  cantnf  9665  wemapwe  9669  cnfcom3lem  9675  ttrcltr  9688  rnttrcl  9694  infxpen  10010  dfac8alem  10025  dfac8clem  10028  ac5num  10032  acni2  10042  numacn  10045  acndom  10047  aceq3lem  10116  dfac5  10124  dfac9  10132  dfac13  10138  fin2i  10290  isfin2-2  10314  fin23lem27  10323  isfin3ds  10324  fin23lem17  10333  fin23lem39  10345  isf33lem  10361  isf34lem7  10374  isf34lem6  10375  fin1a2lem10  10404  fin1a2lem12  10406  hsmexlem4  10424  axcc2lem  10431  axcc3  10433  domtriomlem  10437  axdc2lem  10443  axdc3lem2  10446  axdc3lem3  10447  axdc3lem4  10448  axdc3  10449  axdc4lem  10450  axcclem  10452  ac6num  10474  ac6c4  10476  iundom2g  10535  fpwwe2  10639  pwfseqlem1  10654  pwfseqlem4a  10657  pwfseqlem4  10658  ltapi  10899  ltmpi  10900  fzsubel  13600  elfzp1b  13641  axdc4uzlem  14032  wrd2ind  14777  smuval  16556  prdsbasprj  17542  xpsfrnel  17633  ismri2dad  17710  mreexd  17715  mreacs  17731  iscat  17745  iscatd  17746  iscatd2  17754  catcocl  17758  catpropd  17782  brssc  17888  issubc  17909  subcidcl  17918  subccocl  17919  isfunc  17938  isfuncd  17939  cofucl  17962  funcres2b  17971  fuciso  18052  yonedalem3  18353  yonffthlem  18355  ismgm  18716  ismgmd  18727  issstrmgm  18728  issgrpd  18809  ismndd  18835  eqgfval  19267  efgsdm  19823  efgsdmi  19825  efgsrel  19827  efgsp1  19830  efgsres  19831  dprdfcl  20108  ablfaclem3  20182  isdrngd  20897  isdrngdOLD  20899  issrng  20976  issrngd  20987  islmodd  21016  islbs  21226  lbsind  21230  lbspropd  21249  islbs2  21307  lbsextlem4  21314  lbsextg  21315  pzriprnglem8  21667  zndvds  21728  isphl  21807  isphld  21833  phlpropd  21834  frlmlbs  21976  islindf  21991  islinds2  21992  lindfind  21995  lindsind  21996  lindsind2  21998  lindfrn  22000  lindfmm  22006  lsslindf  22009  mhppwdeg  22342  mat1dimmul  22662  istps  23120  tpspropd  23124  eltpsg  23129  islp  23326  1stcelcls  23647  kgeni  23723  kgencn2  23743  ptpjpre1  23757  elptr2  23760  ptbasin  23763  ptbasfi  23767  ptpjcn  23797  ptpjopn  23798  ptcld  23799  ptcldmpt  23800  ptclsg  23801  ptcnp  23808  qtopval  23881  ptcmplem2  24239  ptcmplem3  24240  ptcmplem4  24241  istmd  24260  istgp  24263  tmdgsum  24281  istlm  24371  isusp  24447  prdsdsf  24553  prdsxmet  24555  isms  24635  mspropd  24660  setsxms  24665  setsms  24666  tmsxms  24672  tmsms  24673  isnrg  24846  tngnrg  24860  bcthlem2  25513  bcthlem3  25514  bcthlem4  25515  bcthlem5  25516  iscms  25533  cmspropd  25537  cmssmscld  25538  cmsss  25539  shft2rab  25696  ovolicc2lem3  25707  ovolicc2lem4  25708  ovolicc2lem5  25709  vitalilem2  25797  vitalilem3  25798  vitali  25801  limcfval  26060  limcmpt2  26072  limcres  26074  cnplimc  26075  cnlimci  26077  elcpn  26122  uc1pval  26326  ig1pcl  26365  jensen  27182  axtgcont  28767  tglngval  28849  ishlg2  28900  ishlg  28903  mirbtwnb  28978  trgcopy  29144  trgcopyeu  29146  acopyeu  29174  isinagd  29185  tgasa1  29204  wlkp1lem3  30052  usgrwwlks2on  30336  umgrwwlks2on  30337  clwwlknon1  30477  clwwlknonclwlknonf1o  30742  imsmet  31072  smcn  31079  iscbn  31245  sbceqbidf  32862  fnpreimac  33044  isslmd  33545  0nellinds  33708  lindssn  33714  lindfpropd  33718  elrspunidl  33759  lbslsat  34029  lindsunlem  34037  brfldext  34058  submateq  34222  lmatcl  34229  ispcmp  34270  zarcmplem  34294  zhmnrg  34378  ismntoplly  34438  sigapildsys  34576  fiunelcarsg  34730  eulerpartlemgvv  34790  eulerpart  34796  fineqvinfep  35554  onvf1odlem2  35604  ptpconn  35738  cvmscbv  35763  cvmshmeo  35776  cvmsss2  35779  cvmliftlem7  35796  cvmliftlem10  35799  cvmlift2lem11  35818  cvmlift2lem12  35819  satffunlem1lem1  35907  satffunlem2lem1  35909  sategoelfvb  35924  prv1n  35936  elmpps  36078  nmulprop  36695  nmulcom  36699  nmulrid  36702  nmuladdel  36717  cbvriotavw2  36781  cbvmpovw2  36787  cbvmpo1vw2  36788  cbvmpo2vw2  36789  cbvixpvw2  36790  cbvitgvw2  36793  cbvsbcdavw2  36803  cbvixpdavw  36823  cbvrmodavw2  36828  cbvreudavw2  36829  cbvmpodavw2  36836  cbvmpo1davw2  36837  cbvmpo2davw2  36838  cbvixpdavw2  36839  cbvproddavw2  36841  cbvitgdavw2  36842  weiunpo  37009  weiunso  37010  weiunfr  37011  weiunse  37012  bj-elabd2ALT  37594  bj-ru1  37612  currysetlem  37614  currysetlem1  37616  bj-ismoore  37780  csbfinxpg  38067  pibt2  38096  lindsadd  38297  lindsenlbs  38299  ptrest  38303  upixp  38413  sdclem1  38427  sstotbnd2  38458  prdsbnd2  38479  isprrngo  38734  isopos  39987  isatl  40106  aks6d1c1p6  42914  isnacs3  43474  nacsfix  43476  mzpclall  43491  dnnumch1  43804  dnwech  43808  aomclem3  43816  aomclem8  43821  dfac11  43822  islmodfg  43829  oaordnr  44056  omnord1  44065  oenord1  44076  cantnfresb  44084  rfovcnvf1od  44763  ismnu  45004  sblpnf  45053  rusbcALT  45181  cbvrabv2w  45879  choicefi  45950  climsuselem1  46356  climsuse  46357  cncfuni  46633  dvnprodlem1  46693  stoweidlem31  46778  stoweidlem59  46806  fourierdlem46  46899  fourierdlem62  46915  fourierdlem72  46925  fourierdlem79  46932  fourierdlem88  46941  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem112  46965  qndenserrnbllem  47041  ioorrnopnlem  47051  ioorrnopn  47052  ioorrnopnxr  47054  issal  47061  subsaliuncllem  47104  subsaliuncl  47105  subsalsal  47106  sge0tsms  47127  sge0iunmpt  47165  sge0seq  47193  ovnsubaddlem1  47317  ovnsubaddlem2  47318  hoidmvlelem3  47344  hoidmvlelem4  47345  rrnmbl  47361  hoiqssbllem3  47371  hspmbl  47376  hoimbl  47378  issmflem  47474  issmfd  47482  issmfdf  47484  smfpimltmpt  47493  issmfled  47504  smfpimltxrmptf  47505  smfmbfcex  47507  issmfgtd  47508  smflimlem1  47518  smflimlem2  47519  smflimlem3  47520  smflimlem6  47523  smfpimgtmpt  47528  smfpimgtxrmptf  47531  smfres  47537  smfpimcclem  47554  smfpimcc  47555  dfateq12d  47896  iscllaw  48987  isprmrng  49134  islininds  49259  brab2ddw  49640  brab2ddw2  49641  funcf2lem  49892  isthincd2lem2  50246  setc1onsubc  50413