Theorem eleq12d 2854

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  neleq12d  3066  cbvraldva2  3336  cdeqel  3733  sbceqbid  3745  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbcel12  4368  elvvuni  5727  elrnmpt1  5941  canth  7375  onnseq  8356  smoeq  8362  smores  8364  smores2  8366  iordsmo  8369  tz7.49  8459  nnaordr  8633  omsmolem  8670  naddel2  8702  fvixp  8934  cbvixp  8946  cbvixpv  8947  mptelixpg  8967  boxcutc  8973  ixpiunwdom  9588  elirr  9598  cantnflt  9677  oemapvali  9689  cantnflem1  9694  cantnf  9698  wemapwe  9702  cnfcom3lem  9708  ttrcltr  9721  rnttrcl  9727  infxpen  10097  dfac8alem  10112  dfac8clem  10115  ac5num  10119  acni2  10129  numacn  10132  acndom  10134  aceq3lem  10203  dfac5  10211  dfac9  10219  dfac13  10225  fin2i  10377  isfin2-2  10401  fin23lem27  10410  isfin3ds  10411  fin23lem17  10420  fin23lem39  10432  isf33lem  10448  isf34lem7  10461  isf34lem6  10462  fin1a2lem10  10491  fin1a2lem12  10493  hsmexlem4  10511  axcc2lem  10518  axcc3  10520  domtriomlem  10524  axdc2lem  10530  axdc3lem2  10533  axdc3lem3  10534  axdc3lem4  10535  axdc3  10536  axdc4lem  10537  axcclem  10539  ac6num  10561  ac6c4  10563  iundom2g  10628  fpwwe2  10732  pwfseqlem1  10747  pwfseqlem4a  10750  pwfseqlem4  10751  ltapi  10992  ltmpi  10993  fzsubel  13698  elfzp1b  13739  axdc4uzlem  14130  wrd2ind  14877  smuval  16657  prdsbasprj  17649  xpsfrnel  17740  ismri2dad  17817  mreexd  17822  mreacs  17838  iscat  17852  iscatd  17853  iscatd2  17861  catcocl  17865  catpropd  17889  brssc  17995  issubc  18016  subcidcl  18025  subccocl  18026  isfunc  18045  isfuncd  18046  cofucl  18069  funcres2b  18078  fuciso  18159  yonedalem3  18460  yonffthlem  18462  ismgm  18823  ismgmd  18836  issstrmgm  18837  issgrpd  18925  ismndd  18952  eqgfval  19394  efgsdm  19950  efgsdmi  19952  efgsrel  19954  efgsp1  19957  efgsres  19958  dprdfcl  20235  ablfaclem3  20309  isdrngd  21028  isdrngdOLD  21030  issrng  21107  issrngd  21118  islmodd  21147  islbs  21357  lbsind  21361  lbspropd  21380  islbs2  21438  lbsextlem4  21445  lbsextg  21446  pzriprnglem8  21800  zndvds  21861  isphl  21940  isphld  21966  phlpropd  21967  frlmlbs  22109  islindf  22124  islinds2  22125  lindfind  22128  lindsind  22129  lindsind2  22131  lindfrn  22133  lindfmm  22139  lsslindf  22142  lindsenlbs  22163  mhppwdeg  22477  mat1dimmul  22797  istps  23258  tpspropd  23262  eltpsg  23267  islp  23464  1stcelcls  23786  kgeni  23862  kgencn2  23882  ptpjpre1  23896  elptr2  23899  ptbasin  23902  ptbasfi  23906  ptpjcn  23936  ptpjopn  23937  ptcld  23938  ptcldmpt  23939  ptclsg  23940  ptcnp  23947  qtopval  24020  ptcmplem2  24378  ptcmplem3  24379  ptcmplem4  24380  istmd  24399  istgp  24402  tmdgsum  24420  istlm  24510  isusp  24586  prdsdsf  24692  prdsxmet  24694  isms  24774  mspropd  24799  setsxms  24804  setsms  24805  tmsxms  24811  tmsms  24812  isnrg  24985  tngnrg  24999  bcthlem2  25652  bcthlem3  25653  bcthlem4  25654  bcthlem5  25655  iscms  25672  cmspropd  25676  cmssmscld  25677  cmsss  25678  shft2rab  25835  ovolicc2lem3  25846  ovolicc2lem4  25847  ovolicc2lem5  25848  vitalilem2  25936  vitalilem3  25937  vitali  25940  limcfval  26198  limcmpt2  26210  limcres  26212  cnplimc  26213  cnlimci  26215  elcpn  26260  uc1pval  26464  ig1pcl  26503  jensen  27322  axtgcont  28937  tglngval  29020  ishlg2  29071  ishlg  29074  mirbtwnb  29150  trgcopy  29317  trgcopyeu  29319  acopyeu  29348  isinagd  29364  tgasa1  29409  wlkp1lem3  30260  usgrwwlks2on  30553  umgrwwlks2on  30554  clwwlknon1  30694  clwwlknonclwlknonf1o  30969  imsmet  31299  smcn  31306  iscbn  31472  tgextahpl  33075  tgextancgra  33080  sbceqbidf  33131  fnpreimac  33312  isslmd  33810  0nellinds  33973  lindssn  33980  lindfpropd  33984  elrspunidl  34025  lbslsat  34295  lindsunlem  34303  brfldext  34324  submateq  34488  lmatcl  34495  ispcmp  34536  zarcmplem  34560  zhmnrg  34644  ismntoplly  34704  sigapildsys  34842  fiunelcarsg  34995  eulerpartlemgvv  35055  eulerpart  35061  fineqvinfep  35850  brlexod  35939  brr0d  35941  onvf1odlem2  35952  ptpconn  36085  cvmscbv  36110  cvmshmeo  36123  cvmsss2  36126  cvmliftlem7  36143  cvmliftlem10  36146  cvmlift2lem11  36165  cvmlift2lem12  36166  satffunlem1lem1  36254  satffunlem2lem1  36256  sategoelfvb  36271  prv1n  36283  elmpps  36425  mirimanoffr  36547  nmulprop  37032  nmulcom  37036  nmulrid  37039  nmuladdel  37054  cbvriotavw2  37118  cbvmpovw2  37124  cbvmpo1vw2  37125  cbvmpo2vw2  37126  cbvixpvw2  37127  cbvitgvw2  37130  cbvsbcdavw2  37140  cbvixpdavw  37160  cbvrmodavw2  37165  cbvreudavw2  37166  cbvmpodavw2  37173  cbvmpo1davw2  37174  cbvmpo2davw2  37175  cbvixpdavw2  37176  cbvproddavw2  37178  cbvitgdavw2  37179  weiunpo  37346  weiunso  37347  weiunfr  37348  weiunse  37349  bj-elabd2ALT  37931  bj-ru1  37949  currysetlem  37951  currysetlem1  37953  bj-ismoore  38119  csbfinxpg  38405  pibt2  38434  lindsadd  38630  ptrest  38631  upixp  38757  sdclem1  38771  sstotbnd2  38802  prdsbnd2  38823  isprrngo  39078  isopos  40331  isatl  40450  aks6d1c1p6  43258  isnacs3  43815  nacsfix  43817  mzpclall  43832  dnnumch1  44145  dnwech  44149  aomclem3  44152  aomclem8  44157  dfac11  44158  islmodfg  44165  oaordnr  44392  omnord1  44401  oenord1  44412  cantnfresb  44420  rfovcnvf1od  45098  ismnu  45339  sblpnf  45388  rusbcALT  45516  cbvrabv2w  46237  choicefi  46308  climsuselem1  46713  climsuse  46714  cncfuni  46990  dvnprodlem1  47050  stoweidlem31  47135  stoweidlem59  47163  fourierdlem46  47256  fourierdlem62  47272  fourierdlem72  47282  fourierdlem79  47289  fourierdlem88  47298  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem112  47322  qndenserrnbllem  47398  ioorrnopnlem  47408  ioorrnopn  47409  ioorrnopnxr  47411  issal  47418  subsaliuncllem  47461  subsaliuncl  47462  subsalsal  47463  sge0tsms  47484  sge0iunmpt  47522  sge0seq  47550  ovnsubaddlem1  47674  ovnsubaddlem2  47675  hoidmvlelem3  47701  hoidmvlelem4  47702  rrnmbl  47718  hoiqssbllem3  47728  hspmbl  47733  hoimbl  47735  issmflem  47831  issmfd  47839  issmfdf  47841  smfpimltmpt  47850  issmfled  47861  smfpimltxrmptf  47862  smfmbfcex  47864  issmfgtd  47865  smflimlem1  47875  smflimlem2  47876  smflimlem3  47877  smflimlem6  47880  smfpimgtmpt  47885  smfpimgtxrmptf  47888  smfres  47894  smfpimcclem  47911  smfpimcc  47912  dfateq12d  48290  iscllaw  49380  isprmrng  49527  islininds  49652  brab2ddw  50034  brab2ddw2  50035  funcf2lem  50289  isthincd2lem2  50664  setc1onsubc  50834