Theorem eleq12d 2820

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ∈ wcel 2099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-clel 2803

This theorem is referenced by:  neleq12d  3041  cbvraldva2  3333  cbvrexdva2OLD  3335  cdeqel  3770  ru  3774  ruOLD  3775  sbceqbid  3783  cbvrabcsfw  3936  cbvralcsf  3937  cbvreucsf  3939  cbvrabcsf  3940  sbcel12  4406  elvvuni  5749  elrnmpt1  5955  canth  7367  onnseq  8364  smoeq  8370  smores  8372  smores2  8374  iordsmo  8377  tz7.49  8465  nnaordr  8640  omsmolem  8677  naddel2  8708  fvixp  8921  cbvixp  8933  mptelixpg  8954  boxcutc  8960  ixpiunwdom  9624  elirr  9631  cantnflt  9706  oemapvali  9718  cantnflem1  9723  cantnf  9727  wemapwe  9731  cnfcom3lem  9737  ttrcltr  9750  rnttrcl  9756  infxpen  10048  dfac8alem  10063  dfac8clem  10066  ac5num  10070  acni2  10080  numacn  10083  acndom  10085  aceq3lem  10154  dfac5  10162  dfac9  10170  dfac13  10176  fin2i  10327  isfin2-2  10351  fin23lem27  10360  isfin3ds  10361  fin23lem17  10370  fin23lem39  10382  isf33lem  10398  isf34lem7  10411  isf34lem6  10412  fin1a2lem10  10441  fin1a2lem12  10443  hsmexlem4  10461  axcc2lem  10468  axcc3  10470  domtriomlem  10474  axdc2lem  10480  axdc3lem2  10483  axdc3lem3  10484  axdc3lem4  10485  axdc3  10486  axdc4lem  10487  axcclem  10489  ac6num  10511  ac6c4  10513  iundom2g  10572  fpwwe2  10675  pwfseqlem1  10690  pwfseqlem4a  10693  pwfseqlem4  10694  ltapi  10935  ltmpi  10936  eluzaddOLD  12901  fzsubel  13583  elfzp1b  13624  axdc4uzlem  13995  wrd2ind  14724  smuval  16474  prdsbasprj  17480  xpsfrnel  17570  ismri2dad  17643  mreexd  17648  mreacs  17664  iscat  17678  iscatd  17679  iscatd2  17687  catcocl  17691  catpropd  17715  brssc  17823  issubc  17847  subcidcl  17856  subccocl  17857  isfunc  17876  isfuncd  17877  cofucl  17900  funcres2b  17909  fuciso  17993  yonedalem3  18298  yonffthlem  18300  ismgm  18627  ismgmd  18638  issstrmgm  18639  issgrpd  18716  ismndd  18742  eqgfval  19164  efgsdm  19722  efgsdmi  19724  efgsrel  19726  efgsp1  19729  efgsres  19730  dprdfcl  20007  ablfaclem3  20081  isdrngd  20737  isdrngdOLD  20739  issrng  20817  issrngd  20828  islmodd  20836  islbs  21048  lbsind  21052  lbspropd  21071  islbs2  21129  lbsextlem4  21136  lbsextg  21137  pzriprnglem8  21472  zndvds  21541  isphl  21618  isphld  21644  phlpropd  21645  frlmlbs  21789  islindf  21804  islinds2  21805  lindfind  21808  lindsind  21809  lindsind2  21811  lindfrn  21813  lindfmm  21819  lsslindf  21822  mhppwdeg  22138  mat1dimmul  22464  istps  22922  tpspropd  22926  eltpsg  22931  eltpsgOLD  22932  islp  23130  1stcelcls  23451  kgeni  23527  kgencn2  23547  ptpjpre1  23561  elptr2  23564  ptbasin  23567  ptbasfi  23571  ptpjcn  23601  ptpjopn  23602  ptcld  23603  ptcldmpt  23604  ptclsg  23605  ptcnp  23612  qtopval  23685  ptcmplem2  24043  ptcmplem3  24044  ptcmplem4  24045  istmd  24064  istgp  24067  tmdgsum  24085  istlm  24175  isusp  24252  prdsdsf  24359  prdsxmet  24361  isms  24441  mspropd  24466  setsxms  24473  setsms  24474  tmsxms  24481  tmsms  24482  isnrg  24663  tngnrg  24677  bcthlem2  25339  bcthlem3  25340  bcthlem4  25341  bcthlem5  25342  iscms  25359  cmspropd  25363  cmssmscld  25364  cmsss  25365  shft2rab  25523  ovolicc2lem3  25534  ovolicc2lem4  25535  ovolicc2lem5  25536  vitalilem2  25624  vitalilem3  25625  vitali  25628  limcfval  25887  limcmpt2  25899  limcres  25901  cnplimc  25902  cnlimci  25904  elcpn  25950  uc1pval  26162  ig1pcl  26201  jensen  27012  axtgcont  28391  tglngval  28473  ishlg  28524  mirbtwnb  28594  trgcopy  28726  trgcopyeu  28728  acopyeu  28756  isinagd  28761  tgasa1  28780  wlkp1lem3  29607  umgrwwlks2on  29886  clwwlknon1  30025  clwwlknonclwlknonf1o  30290  imsmet  30619  smcn  30626  iscbn  30792  sbceqbidf  32410  fnpreimac  32586  isslmd  33068  0nellinds  33249  lindssn  33257  lindfpropd  33261  elrspunidl  33307  lbslsat  33515  lindsunlem  33523  brfldext  33540  submateq  33635  lmatcl  33642  ispcmp  33683  zarcmplem  33707  zhmnrg  33793  ismntoplly  33851  sigapildsys  34006  fiunelcarsg  34161  eulerpartlemgvv  34221  eulerpart  34227  ptpconn  35072  cvmscbv  35097  cvmshmeo  35110  cvmsss2  35113  cvmliftlem7  35130  cvmliftlem10  35133  cvmlift2lem11  35152  cvmlift2lem12  35153  satffunlem1lem1  35241  satffunlem2lem1  35243  sategoelfvb  35258  prv1n  35270  elmpps  35412  bj-elabd2ALT  36642  currysetlem  36663  currysetlem1  36665  bj-ismoore  36823  csbfinxpg  37106  pibt2  37135  lindsadd  37325  lindsenlbs  37327  ptrest  37331  upixp  37441  sdclem1  37455  sstotbnd2  37486  prdsbnd2  37507  isprrngo  37762  isopos  38889  isatl  39008  aks6d1c1p6  41824  isnacs3  42402  nacsfix  42404  mzpclall  42419  dnnumch1  42740  dnwech  42744  aomclem3  42752  aomclem8  42757  dfac11  42758  islmodfg  42765  oaordnr  42997  omnord1  43006  oenord1  43017  cantnfresb  43025  rfovcnvf1od  43706  ismnu  43970  sblpnf  44019  rusbcALT  44148  choicefi  44841  climsuselem1  45262  climsuse  45263  cncfuni  45541  dvnprodlem1  45601  stoweidlem31  45686  stoweidlem59  45714  fourierdlem46  45807  fourierdlem62  45823  fourierdlem72  45833  fourierdlem79  45840  fourierdlem88  45849  fourierdlem89  45850  fourierdlem90  45851  fourierdlem91  45852  fourierdlem112  45873  qndenserrnbllem  45949  ioorrnopnlem  45959  ioorrnopn  45960  ioorrnopnxr  45962  issal  45969  subsaliuncllem  46012  subsaliuncl  46013  subsalsal  46014  sge0tsms  46035  sge0iunmpt  46073  sge0seq  46101  ovnsubaddlem1  46225  ovnsubaddlem2  46226  hoidmvlelem3  46252  hoidmvlelem4  46253  rrnmbl  46269  hoiqssbllem3  46279  hspmbl  46284  hoimbl  46286  issmflem  46382  issmfd  46390  issmfdf  46392  smfpimltmpt  46401  issmfled  46412  smfpimltxrmptf  46413  smfmbfcex  46415  issmfgtd  46416  smflimlem1  46426  smflimlem2  46427  smflimlem3  46428  smflimlem6  46431  smfpimgtmpt  46436  smfpimgtxrmptf  46439  smfres  46445  smfpimcclem  46462  smfpimcc  46463  dfateq12d  46773  iscllaw  47600  islininds  47863  funcf2lem  48373  isthincd2lem2  48391