Theorem eleq12d 2855

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

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

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 2147  ax-9 2155  ax-ext 2733

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

This theorem is used by:  neleq12d  3067  cbvraldva2  3337  cdeqel  3734  sbceqbid  3746  cbvrabcsfw  3888  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  sbcel12  4369  elvvuni  5728  elrnmpt1  5942  canth  7372  onnseq  8345  smoeq  8351  smores  8353  smores2  8355  iordsmo  8358  tz7.49  8448  nnaordr  8622  omsmolem  8659  naddel2  8691  fvixp  8923  cbvixp  8935  cbvixpv  8936  mptelixpg  8956  boxcutc  8962  ixpiunwdom  9577  elirr  9587  cantnflt  9666  oemapvali  9678  cantnflem1  9683  cantnf  9687  wemapwe  9691  cnfcom3lem  9697  ttrcltr  9710  rnttrcl  9716  infxpen  10086  dfac8alem  10101  dfac8clem  10104  ac5num  10108  acni2  10118  numacn  10121  acndom  10123  aceq3lem  10192  dfac5  10200  dfac9  10208  dfac13  10214  fin2i  10366  isfin2-2  10390  fin23lem27  10399  isfin3ds  10400  fin23lem17  10409  fin23lem39  10421  isf33lem  10437  isf34lem7  10450  isf34lem6  10451  fin1a2lem10  10480  fin1a2lem12  10482  hsmexlem4  10500  axcc2lem  10507  axcc3  10509  domtriomlem  10513  axdc2lem  10519  axdc3lem2  10522  axdc3lem3  10523  axdc3lem4  10524  axdc3  10525  axdc4lem  10526  axcclem  10528  ac6num  10550  ac6c4  10552  iundom2g  10617  fpwwe2  10721  pwfseqlem1  10736  pwfseqlem4a  10739  pwfseqlem4  10740  ltapi  10981  ltmpi  10982  fzsubel  13687  elfzp1b  13728  axdc4uzlem  14119  wrd2ind  14865  smuval  16644  prdsbasprj  17636  xpsfrnel  17727  ismri2dad  17804  mreexd  17809  mreacs  17825  iscat  17839  iscatd  17840  iscatd2  17848  catcocl  17852  catpropd  17876  brssc  17982  issubc  18003  subcidcl  18012  subccocl  18013  isfunc  18032  isfuncd  18033  cofucl  18056  funcres2b  18065  fuciso  18146  yonedalem3  18447  yonffthlem  18449  ismgm  18810  ismgmd  18823  issstrmgm  18824  issgrpd  18912  ismndd  18939  eqgfval  19381  efgsdm  19937  efgsdmi  19939  efgsrel  19941  efgsp1  19944  efgsres  19945  dprdfcl  20222  ablfaclem3  20296  isdrngd  21015  isdrngdOLD  21017  issrng  21094  issrngd  21105  islmodd  21134  islbs  21344  lbsind  21348  lbspropd  21367  islbs2  21425  lbsextlem4  21432  lbsextg  21433  pzriprnglem8  21787  zndvds  21848  isphl  21927  isphld  21953  phlpropd  21954  frlmlbs  22096  islindf  22111  islinds2  22112  lindfind  22115  lindsind  22116  lindsind2  22118  lindfrn  22120  lindfmm  22126  lsslindf  22129  lindsenlbs  22150  mhppwdeg  22464  mat1dimmul  22784  istps  23245  tpspropd  23249  eltpsg  23254  islp  23451  1stcelcls  23773  kgeni  23849  kgencn2  23869  ptpjpre1  23883  elptr2  23886  ptbasin  23889  ptbasfi  23893  ptpjcn  23923  ptpjopn  23924  ptcld  23925  ptcldmpt  23926  ptclsg  23927  ptcnp  23934  qtopval  24007  ptcmplem2  24365  ptcmplem3  24366  ptcmplem4  24367  istmd  24386  istgp  24389  tmdgsum  24407  istlm  24497  isusp  24573  prdsdsf  24679  prdsxmet  24681  isms  24761  mspropd  24786  setsxms  24791  setsms  24792  tmsxms  24798  tmsms  24799  isnrg  24972  tngnrg  24986  bcthlem2  25639  bcthlem3  25640  bcthlem4  25641  bcthlem5  25642  iscms  25659  cmspropd  25663  cmssmscld  25664  cmsss  25665  shft2rab  25822  ovolicc2lem3  25833  ovolicc2lem4  25834  ovolicc2lem5  25835  vitalilem2  25923  vitalilem3  25924  vitali  25927  limcfval  26185  limcmpt2  26197  limcres  26199  cnplimc  26200  cnlimci  26202  elcpn  26247  uc1pval  26451  ig1pcl  26490  jensen  27309  axtgcont  28924  tglngval  29007  ishlg2  29058  ishlg  29061  mirbtwnb  29137  trgcopy  29304  trgcopyeu  29306  acopyeu  29335  isinagd  29351  tgasa1  29396  wlkp1lem3  30247  usgrwwlks2on  30540  umgrwwlks2on  30541  clwwlknon1  30681  clwwlknonclwlknonf1o  30956  imsmet  31286  smcn  31293  iscbn  31459  sbceqbidf  33076  fnpreimac  33257  isslmd  33756  0nellinds  33919  lindssn  33926  lindfpropd  33930  elrspunidl  33971  lbslsat  34241  lindsunlem  34249  brfldext  34270  submateq  34434  lmatcl  34441  ispcmp  34482  zarcmplem  34506  zhmnrg  34590  ismntoplly  34650  sigapildsys  34788  fiunelcarsg  34941  eulerpartlemgvv  35001  eulerpart  35007  fineqvinfep  35776  onvf1odlem2  35866  ptpconn  35977  cvmscbv  36002  cvmshmeo  36015  cvmsss2  36018  cvmliftlem7  36035  cvmliftlem10  36038  cvmlift2lem11  36057  cvmlift2lem12  36058  satffunlem1lem1  36146  satffunlem2lem1  36148  sategoelfvb  36163  prv1n  36175  elmpps  36317  nmulprop  36919  nmulcom  36923  nmulrid  36926  nmuladdel  36941  cbvriotavw2  37005  cbvmpovw2  37011  cbvmpo1vw2  37012  cbvmpo2vw2  37013  cbvixpvw2  37014  cbvitgvw2  37017  cbvsbcdavw2  37027  cbvixpdavw  37047  cbvrmodavw2  37052  cbvreudavw2  37053  cbvmpodavw2  37060  cbvmpo1davw2  37061  cbvmpo2davw2  37062  cbvixpdavw2  37063  cbvproddavw2  37065  cbvitgdavw2  37066  weiunpo  37233  weiunso  37234  weiunfr  37235  weiunse  37236  bj-elabd2ALT  37818  bj-ru1  37836  currysetlem  37838  currysetlem1  37840  bj-ismoore  38006  csbfinxpg  38291  pibt2  38320  lindsadd  38516  ptrest  38517  upixp  38643  sdclem1  38657  sstotbnd2  38688  prdsbnd2  38709  isprrngo  38964  isopos  40217  isatl  40336  aks6d1c1p6  43144  isnacs3  43700  nacsfix  43702  mzpclall  43717  dnnumch1  44030  dnwech  44034  aomclem3  44042  aomclem8  44047  dfac11  44048  islmodfg  44055  oaordnr  44282  omnord1  44291  oenord1  44302  cantnfresb  44310  rfovcnvf1od  44989  ismnu  45230  sblpnf  45279  rusbcALT  45407  cbvrabv2w  46112  choicefi  46183  climsuselem1  46588  climsuse  46589  cncfuni  46865  dvnprodlem1  46925  stoweidlem31  47010  stoweidlem59  47038  fourierdlem46  47131  fourierdlem62  47147  fourierdlem72  47157  fourierdlem79  47164  fourierdlem88  47173  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem112  47197  qndenserrnbllem  47273  ioorrnopnlem  47283  ioorrnopn  47284  ioorrnopnxr  47286  issal  47293  subsaliuncllem  47336  subsaliuncl  47337  subsalsal  47338  sge0tsms  47359  sge0iunmpt  47397  sge0seq  47425  ovnsubaddlem1  47549  ovnsubaddlem2  47550  hoidmvlelem3  47576  hoidmvlelem4  47577  rrnmbl  47593  hoiqssbllem3  47603  hspmbl  47608  hoimbl  47610  issmflem  47706  issmfd  47714  issmfdf  47716  smfpimltmpt  47725  issmfled  47736  smfpimltxrmptf  47737  smfmbfcex  47739  issmfgtd  47740  smflimlem1  47750  smflimlem2  47751  smflimlem3  47752  smflimlem6  47755  smfpimgtmpt  47760  smfpimgtxrmptf  47763  smfres  47769  smfpimcclem  47786  smfpimcc  47787  dfateq12d  48165  iscllaw  49255  isprmrng  49402  islininds  49527  brab2ddw  49908  brab2ddw2  49909  funcf2lem  50158  isthincd2lem2  50512  setc1onsubc  50679