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 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 2732

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

This theorem is used by:  neleq12d  3066  cbvraldva2  3336  cdeqel  3734  sbceqbid  3746  cbvrabcsfw  3888  cbvralcsf  3889  cbvreucsf  3891  cbvrabcsf  3892  sbcel12  4369  elvvuni  5732  elrnmpt1  5944  canth  7367  onnseq  8333  smoeq  8339  smores  8341  smores2  8343  iordsmo  8346  tz7.49  8434  nnaordr  8608  omsmolem  8645  naddel2  8677  fvixp  8909  cbvixp  8921  cbvixpv  8922  mptelixpg  8942  boxcutc  8948  ixpiunwdom  9562  elirr  9572  cantnflt  9651  oemapvali  9663  cantnflem1  9668  cantnf  9672  wemapwe  9676  cnfcom3lem  9682  ttrcltr  9695  rnttrcl  9701  infxpen  10017  dfac8alem  10032  dfac8clem  10035  ac5num  10039  acni2  10049  numacn  10052  acndom  10054  aceq3lem  10123  dfac5  10131  dfac9  10139  dfac13  10145  fin2i  10297  isfin2-2  10321  fin23lem27  10330  isfin3ds  10331  fin23lem17  10340  fin23lem39  10352  isf33lem  10368  isf34lem7  10381  isf34lem6  10382  fin1a2lem10  10411  fin1a2lem12  10413  hsmexlem4  10431  axcc2lem  10438  axcc3  10440  domtriomlem  10444  axdc2lem  10450  axdc3lem2  10453  axdc3lem3  10454  axdc3lem4  10455  axdc3  10456  axdc4lem  10457  axcclem  10459  ac6num  10481  ac6c4  10483  iundom2g  10548  fpwwe2  10652  pwfseqlem1  10667  pwfseqlem4a  10670  pwfseqlem4  10671  ltapi  10912  ltmpi  10913  fzsubel  13615  elfzp1b  13656  axdc4uzlem  14047  wrd2ind  14792  smuval  16571  prdsbasprj  17557  xpsfrnel  17648  ismri2dad  17725  mreexd  17730  mreacs  17746  iscat  17760  iscatd  17761  iscatd2  17769  catcocl  17773  catpropd  17797  brssc  17903  issubc  17924  subcidcl  17933  subccocl  17934  isfunc  17953  isfuncd  17954  cofucl  17977  funcres2b  17986  fuciso  18067  yonedalem3  18368  yonffthlem  18370  ismgm  18731  ismgmd  18744  issstrmgm  18745  issgrpd  18832  ismndd  18859  eqgfval  19301  efgsdm  19857  efgsdmi  19859  efgsrel  19861  efgsp1  19864  efgsres  19865  dprdfcl  20142  ablfaclem3  20216  isdrngd  20931  isdrngdOLD  20933  issrng  21010  issrngd  21021  islmodd  21050  islbs  21260  lbsind  21264  lbspropd  21283  islbs2  21341  lbsextlem4  21348  lbsextg  21349  pzriprnglem8  21701  zndvds  21762  isphl  21841  isphld  21867  phlpropd  21868  frlmlbs  22010  islindf  22025  islinds2  22026  lindfind  22029  lindsind  22030  lindsind2  22032  lindfrn  22034  lindfmm  22040  lsslindf  22043  lindsenlbs  22064  mhppwdeg  22378  mat1dimmul  22698  istps  23159  tpspropd  23163  eltpsg  23168  islp  23365  1stcelcls  23687  kgeni  23763  kgencn2  23783  ptpjpre1  23797  elptr2  23800  ptbasin  23803  ptbasfi  23807  ptpjcn  23837  ptpjopn  23838  ptcld  23839  ptcldmpt  23840  ptclsg  23841  ptcnp  23848  qtopval  23921  ptcmplem2  24279  ptcmplem3  24280  ptcmplem4  24281  istmd  24300  istgp  24303  tmdgsum  24321  istlm  24411  isusp  24487  prdsdsf  24593  prdsxmet  24595  isms  24675  mspropd  24700  setsxms  24705  setsms  24706  tmsxms  24712  tmsms  24713  isnrg  24886  tngnrg  24900  bcthlem2  25553  bcthlem3  25554  bcthlem4  25555  bcthlem5  25556  iscms  25573  cmspropd  25577  cmssmscld  25578  cmsss  25579  shft2rab  25736  ovolicc2lem3  25747  ovolicc2lem4  25748  ovolicc2lem5  25749  vitalilem2  25837  vitalilem3  25838  vitali  25841  limcfval  26099  limcmpt2  26111  limcres  26113  cnplimc  26114  cnlimci  26116  elcpn  26161  uc1pval  26365  ig1pcl  26404  jensen  27225  axtgcont  28810  tglngval  28893  ishlg2  28944  ishlg  28947  mirbtwnb  29023  trgcopy  29190  trgcopyeu  29192  acopyeu  29221  isinagd  29237  tgasa1  29282  wlkp1lem3  30133  usgrwwlks2on  30426  umgrwwlks2on  30427  clwwlknon1  30567  clwwlknonclwlknonf1o  30842  imsmet  31172  smcn  31179  iscbn  31345  sbceqbidf  32962  fnpreimac  33143  isslmd  33642  0nellinds  33805  lindssn  33811  lindfpropd  33815  elrspunidl  33856  lbslsat  34126  lindsunlem  34134  brfldext  34155  submateq  34319  lmatcl  34326  ispcmp  34367  zarcmplem  34391  zhmnrg  34475  ismntoplly  34535  sigapildsys  34673  fiunelcarsg  34827  eulerpartlemgvv  34887  eulerpart  34893  fineqvinfep  35651  onvf1odlem2  35701  ptpconn  35812  cvmscbv  35837  cvmshmeo  35850  cvmsss2  35853  cvmliftlem7  35870  cvmliftlem10  35873  cvmlift2lem11  35892  cvmlift2lem12  35893  satffunlem1lem1  35981  satffunlem2lem1  35983  sategoelfvb  35998  prv1n  36010  elmpps  36152  nmulprop  36770  nmulcom  36774  nmulrid  36777  nmuladdel  36792  cbvriotavw2  36856  cbvmpovw2  36862  cbvmpo1vw2  36863  cbvmpo2vw2  36864  cbvixpvw2  36865  cbvitgvw2  36868  cbvsbcdavw2  36878  cbvixpdavw  36898  cbvrmodavw2  36903  cbvreudavw2  36904  cbvmpodavw2  36911  cbvmpo1davw2  36912  cbvmpo2davw2  36913  cbvixpdavw2  36914  cbvproddavw2  36916  cbvitgdavw2  36917  weiunpo  37084  weiunso  37085  weiunfr  37086  weiunse  37087  bj-elabd2ALT  37669  bj-ru1  37687  currysetlem  37689  currysetlem1  37691  bj-ismoore  37855  csbfinxpg  38142  pibt2  38171  lindsadd  38367  ptrest  38368  upixp  38479  sdclem1  38493  sstotbnd2  38524  prdsbnd2  38545  isprrngo  38800  isopos  40053  isatl  40172  aks6d1c1p6  42980  isnacs3  43555  nacsfix  43557  mzpclall  43572  dnnumch1  43885  dnwech  43889  aomclem3  43897  aomclem8  43902  dfac11  43903  islmodfg  43910  oaordnr  44137  omnord1  44146  oenord1  44157  cantnfresb  44165  rfovcnvf1od  44844  ismnu  45085  sblpnf  45134  rusbcALT  45262  cbvrabv2w  45960  choicefi  46031  climsuselem1  46437  climsuse  46438  cncfuni  46714  dvnprodlem1  46774  stoweidlem31  46859  stoweidlem59  46887  fourierdlem46  46980  fourierdlem62  46996  fourierdlem72  47006  fourierdlem79  47013  fourierdlem88  47022  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem112  47046  qndenserrnbllem  47122  ioorrnopnlem  47132  ioorrnopn  47133  ioorrnopnxr  47135  issal  47142  subsaliuncllem  47185  subsaliuncl  47186  subsalsal  47187  sge0tsms  47208  sge0iunmpt  47246  sge0seq  47274  ovnsubaddlem1  47398  ovnsubaddlem2  47399  hoidmvlelem3  47425  hoidmvlelem4  47426  rrnmbl  47442  hoiqssbllem3  47452  hspmbl  47457  hoimbl  47459  issmflem  47555  issmfd  47563  issmfdf  47565  smfpimltmpt  47574  issmfled  47585  smfpimltxrmptf  47586  smfmbfcex  47588  issmfgtd  47589  smflimlem1  47599  smflimlem2  47600  smflimlem3  47601  smflimlem6  47604  smfpimgtmpt  47609  smfpimgtxrmptf  47612  smfres  47618  smfpimcclem  47635  smfpimcc  47636  dfateq12d  48014  iscllaw  49104  isprmrng  49251  islininds  49376  brab2ddw  49757  brab2ddw2  49758  funcf2lem  50007  isthincd2lem2  50361  setc1onsubc  50528