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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840

This theorem is referenced by:  neleq12d  3069  cbvraldva2  3341  cdeqel  3742  sbceqbid  3754  cbvrabcsfw  3896  cbvralcsf  3897  cbvreucsf  3899  cbvrabcsf  3900  sbcel12  4368  elvvuni  5728  elrnmpt1  5940  canth  7354  onnseq  8319  smoeq  8325  smores  8327  smores2  8329  iordsmo  8332  tz7.49  8420  nnaordr  8594  omsmolem  8631  naddel2  8663  fvixp  8888  cbvixp  8900  cbvixpv  8901  mptelixpg  8921  boxcutc  8927  ixpiunwdom  9540  elirr  9550  cantnflt  9629  oemapvali  9641  cantnflem1  9646  cantnf  9650  wemapwe  9654  cnfcom3lem  9660  ttrcltr  9673  rnttrcl  9679  infxpen  9986  dfac8alem  10001  dfac8clem  10004  ac5num  10008  acni2  10018  numacn  10021  acndom  10023  aceq3lem  10092  dfac5  10100  dfac9  10108  dfac13  10114  fin2i  10267  isfin2-2  10291  fin23lem27  10300  isfin3ds  10301  fin23lem17  10310  fin23lem39  10322  isf33lem  10338  isf34lem7  10351  isf34lem6  10352  fin1a2lem10  10381  fin1a2lem12  10383  hsmexlem4  10401  axcc2lem  10408  axcc3  10410  domtriomlem  10414  axdc2lem  10420  axdc3lem2  10423  axdc3lem3  10424  axdc3lem4  10425  axdc3  10426  axdc4lem  10427  axcclem  10429  ac6num  10451  ac6c4  10453  iundom2g  10512  fpwwe2  10616  pwfseqlem1  10631  pwfseqlem4a  10634  pwfseqlem4  10635  ltapi  10876  ltmpi  10877  fzsubel  13576  elfzp1b  13617  axdc4uzlem  14007  wrd2ind  14748  smuval  16527  prdsbasprj  17513  xpsfrnel  17604  ismri2dad  17681  mreexd  17686  mreacs  17702  iscat  17716  iscatd  17717  iscatd2  17725  catcocl  17729  catpropd  17753  brssc  17859  issubc  17880  subcidcl  17889  subccocl  17890  isfunc  17909  isfuncd  17910  cofucl  17933  funcres2b  17942  fuciso  18023  yonedalem3  18324  yonffthlem  18326  ismgm  18687  ismgmd  18698  issstrmgm  18699  issgrpd  18776  ismndd  18802  eqgfval  19232  efgsdm  19788  efgsdmi  19790  efgsrel  19792  efgsp1  19795  efgsres  19796  dprdfcl  20073  ablfaclem3  20147  isdrngd  20835  isdrngdOLD  20837  issrng  20913  issrngd  20924  islmodd  20953  islbs  21163  lbsind  21167  lbspropd  21186  islbs2  21244  lbsextlem4  21251  lbsextg  21252  pzriprnglem8  21595  zndvds  21656  isphl  21735  isphld  21761  phlpropd  21762  frlmlbs  21904  islindf  21919  islinds2  21920  lindfind  21923  lindsind  21924  lindsind2  21926  lindfrn  21928  lindfmm  21934  lsslindf  21937  mhppwdeg  22270  mat1dimmul  22590  istps  23048  tpspropd  23052  eltpsg  23057  islp  23254  1stcelcls  23575  kgeni  23651  kgencn2  23671  ptpjpre1  23685  elptr2  23688  ptbasin  23691  ptbasfi  23695  ptpjcn  23725  ptpjopn  23726  ptcld  23727  ptcldmpt  23728  ptclsg  23729  ptcnp  23736  qtopval  23809  ptcmplem2  24167  ptcmplem3  24168  ptcmplem4  24169  istmd  24188  istgp  24191  tmdgsum  24209  istlm  24299  isusp  24375  prdsdsf  24481  prdsxmet  24483  isms  24563  mspropd  24588  setsxms  24593  setsms  24594  tmsxms  24600  tmsms  24601  isnrg  24774  tngnrg  24788  bcthlem2  25441  bcthlem3  25442  bcthlem4  25443  bcthlem5  25444  iscms  25461  cmspropd  25465  cmssmscld  25466  cmsss  25467  shft2rab  25624  ovolicc2lem3  25635  ovolicc2lem4  25636  ovolicc2lem5  25637  vitalilem2  25725  vitalilem3  25726  vitali  25729  limcfval  25988  limcmpt2  26000  limcres  26002  cnplimc  26003  cnlimci  26005  elcpn  26050  uc1pval  26254  ig1pcl  26293  jensen  27107  axtgcont  28692  tglngval  28774  ishlg  28825  mirbtwnb  28899  trgcopy  29052  trgcopyeu  29054  acopyeu  29082  isinagd  29087  tgasa1  29106  wlkp1lem3  29928  usgrwwlks2on  30212  umgrwwlks2on  30213  clwwlknon1  30353  clwwlknonclwlknonf1o  30618  imsmet  30948  smcn  30955  iscbn  31121  sbceqbidf  32739  fnpreimac  32923  isslmd  33430  0nellinds  33595  lindssn  33602  lindfpropd  33606  elrspunidl  33647  lbslsat  33918  lindsunlem  33926  brfldext  33947  submateq  34111  lmatcl  34118  ispcmp  34159  zarcmplem  34183  zhmnrg  34267  ismntoplly  34327  sigapildsys  34464  fiunelcarsg  34618  eulerpartlemgvv  34678  eulerpart  34684  fineqvinfep  35428  onvf1odlem2  35454  ptpconn  35591  cvmscbv  35616  cvmshmeo  35629  cvmsss2  35632  cvmliftlem7  35649  cvmliftlem10  35652  cvmlift2lem11  35671  cvmlift2lem12  35672  satffunlem1lem1  35760  satffunlem2lem1  35762  sategoelfvb  35777  prv1n  35789  elmpps  35931  nmulprop  36548  nmulcom  36552  cbvriotavw2  36604  cbvmpovw2  36610  cbvmpo1vw2  36611  cbvmpo2vw2  36612  cbvixpvw2  36613  cbvitgvw2  36616  cbvsbcdavw2  36626  cbvixpdavw  36646  cbvrmodavw2  36651  cbvreudavw2  36652  cbvmpodavw2  36659  cbvmpo1davw2  36660  cbvmpo2davw2  36661  cbvixpdavw2  36662  cbvproddavw2  36664  cbvitgdavw2  36665  weiunpo  36833  weiunso  36834  weiunfr  36835  weiunse  36836  bj-elabd2ALT  37417  bj-ru1  37435  currysetlem  37437  currysetlem1  37439  bj-ismoore  37602  csbfinxpg  37889  pibt2  37918  lindsadd  38119  lindsenlbs  38121  ptrest  38125  upixp  38235  sdclem1  38249  sstotbnd2  38280  prdsbnd2  38301  isprrngo  38556  isopos  39811  isatl  39930  aks6d1c1p6  42738  isnacs3  43298  nacsfix  43300  mzpclall  43315  dnnumch1  43628  dnwech  43632  aomclem3  43640  aomclem8  43645  dfac11  43646  islmodfg  43653  oaordnr  43880  omnord1  43889  oenord1  43900  cantnfresb  43908  rfovcnvf1od  44587  ismnu  44830  sblpnf  44879  rusbcALT  45007  cbvrabv2w  45705  choicefi  45776  climsuselem1  46182  climsuse  46183  cncfuni  46459  dvnprodlem1  46519  stoweidlem31  46604  stoweidlem59  46632  fourierdlem46  46725  fourierdlem62  46741  fourierdlem72  46751  fourierdlem79  46758  fourierdlem88  46767  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem112  46791  qndenserrnbllem  46867  ioorrnopnlem  46877  ioorrnopn  46878  ioorrnopnxr  46880  issal  46887  subsaliuncllem  46930  subsaliuncl  46931  subsalsal  46932  sge0tsms  46953  sge0iunmpt  46991  sge0seq  47019  ovnsubaddlem1  47143  ovnsubaddlem2  47144  hoidmvlelem3  47170  hoidmvlelem4  47171  rrnmbl  47187  hoiqssbllem3  47197  hspmbl  47202  hoimbl  47204  issmflem  47300  issmfd  47308  issmfdf  47310  smfpimltmpt  47319  issmfled  47330  smfpimltxrmptf  47331  smfmbfcex  47333  issmfgtd  47334  smflimlem1  47344  smflimlem2  47345  smflimlem3  47346  smflimlem6  47349  smfpimgtmpt  47354  smfpimgtxrmptf  47357  smfres  47363  smfpimcclem  47380  smfpimcc  47381  dfateq12d  47719  iscllaw  48810  isprmrng  48957  islininds  49078  brab2ddw  49459  brab2ddw2  49460  funcf2lem  49711  isthincd2lem2  50065  setc1onsubc  50232