Theorem eleq12d 2828

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  neleq12d  3052  cbvraldva2  3345  cbvrexdva2OLD  3347  cdeqel  3772  ru  3776  sbceqbid  3784  cbvrabcsfw  3937  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  sbcel12  4408  elvvuni  5751  elrnmpt1  5956  canth  7359  onnseq  8341  smoeq  8347  smores  8349  smores2  8351  iordsmo  8354  tz7.49  8442  nnaordr  8617  omsmolem  8653  naddel2  8684  fvixp  8893  cbvixp  8905  mptelixpg  8926  boxcutc  8932  ixpiunwdom  9582  elirr  9589  cantnflt  9664  oemapvali  9676  cantnflem1  9681  cantnf  9685  wemapwe  9689  cnfcom3lem  9695  ttrcltr  9708  rnttrcl  9714  infxpen  10006  dfac8alem  10021  dfac8clem  10024  ac5num  10028  acni2  10038  numacn  10041  acndom  10043  aceq3lem  10112  dfac5  10120  dfac9  10128  dfac13  10134  fin2i  10287  isfin2-2  10311  fin23lem27  10320  isfin3ds  10321  fin23lem17  10330  fin23lem39  10342  isf33lem  10358  isf34lem7  10371  isf34lem6  10372  fin1a2lem10  10401  fin1a2lem12  10403  hsmexlem4  10421  axcc2lem  10428  axcc3  10430  domtriomlem  10434  axdc2lem  10440  axdc3lem2  10443  axdc3lem3  10444  axdc3lem4  10445  axdc3  10446  axdc4lem  10447  axcclem  10449  ac6num  10471  ac6c4  10473  iundom2g  10532  fpwwe2  10635  pwfseqlem1  10650  pwfseqlem4a  10653  pwfseqlem4  10654  ltapi  10895  ltmpi  10896  eluzaddOLD  12854  fzsubel  13534  elfzp1b  13575  axdc4uzlem  13945  wrd2ind  14670  smuval  16419  prdsbasprj  17415  xpsfrnel  17505  ismri2dad  17578  mreexd  17583  mreacs  17599  iscat  17613  iscatd  17614  iscatd2  17622  catcocl  17626  catpropd  17650  brssc  17758  issubc  17782  subcidcl  17791  subccocl  17792  isfunc  17811  isfuncd  17812  cofucl  17835  funcres2b  17844  fuciso  17925  yonedalem3  18230  yonffthlem  18232  ismgm  18559  issstrmgm  18569  issgrpd  18618  ismndd  18644  eqgfval  19051  efgsdm  19593  efgsdmi  19595  efgsrel  19597  efgsp1  19600  efgsres  19601  dprdfcl  19878  ablfaclem3  19952  isdrngd  20341  isdrngdOLD  20343  issrng  20451  issrngd  20462  islmodd  20470  islbs  20680  lbsind  20684  lbspropd  20703  islbs2  20760  lbsextlem4  20767  lbsextg  20768  zndvds  21097  isphl  21173  isphld  21199  phlpropd  21200  frlmlbs  21344  islindf  21359  islinds2  21360  lindfind  21363  lindsind  21364  lindsind2  21366  lindfrn  21368  lindfmm  21374  lsslindf  21377  mhppwdeg  21685  mat1dimmul  21970  istps  22428  tpspropd  22432  eltpsg  22437  eltpsgOLD  22438  islp  22636  1stcelcls  22957  kgeni  23033  kgencn2  23053  ptpjpre1  23067  elptr2  23070  ptbasin  23073  ptbasfi  23077  ptpjcn  23107  ptpjopn  23108  ptcld  23109  ptcldmpt  23110  ptclsg  23111  ptcnp  23118  qtopval  23191  ptcmplem2  23549  ptcmplem3  23550  ptcmplem4  23551  istmd  23570  istgp  23573  tmdgsum  23591  istlm  23681  isusp  23758  prdsdsf  23865  prdsxmet  23867  isms  23947  mspropd  23972  setsxms  23979  setsms  23980  tmsxms  23987  tmsms  23988  isnrg  24169  tngnrg  24183  bcthlem2  24834  bcthlem3  24835  bcthlem4  24836  bcthlem5  24837  iscms  24854  cmspropd  24858  cmssmscld  24859  cmsss  24860  shft2rab  25017  ovolicc2lem3  25028  ovolicc2lem4  25029  ovolicc2lem5  25030  vitalilem2  25118  vitalilem3  25119  vitali  25122  limcfval  25381  limcmpt2  25393  limcres  25395  cnplimc  25396  cnlimci  25398  elcpn  25443  uc1pval  25649  ig1pcl  25685  jensen  26483  axtgcont  27710  tglngval  27792  ishlg  27843  mirbtwnb  27913  trgcopy  28045  trgcopyeu  28047  acopyeu  28075  isinagd  28080  tgasa1  28099  wlkp1lem3  28922  umgrwwlks2on  29201  clwwlknon1  29340  clwwlknonclwlknonf1o  29605  imsmet  29932  smcn  29939  iscbn  30105  sbceqbidf  31715  fnpreimac  31884  isslmd  32335  0nellinds  32472  lindssn  32483  lindfpropd  32487  elrspunidl  32535  lbslsat  32690  lindsunlem  32698  brfldext  32715  submateq  32778  lmatcl  32785  ispcmp  32826  zarcmplem  32850  zhmnrg  32936  ismntoplly  32994  sigapildsys  33149  fiunelcarsg  33304  eulerpartlemgvv  33364  eulerpart  33370  ptpconn  34213  cvmscbv  34238  cvmshmeo  34251  cvmsss2  34254  cvmliftlem7  34271  cvmliftlem10  34274  cvmlift2lem11  34293  cvmlift2lem12  34294  satffunlem1lem1  34382  satffunlem2lem1  34384  sategoelfvb  34399  prv1n  34411  elmpps  34553  bj-elabd2ALT  35794  currysetlem  35815  currysetlem1  35817  bj-ismoore  35975  csbfinxpg  36258  pibt2  36287  lindsadd  36470  lindsenlbs  36472  ptrest  36476  upixp  36586  sdclem1  36600  sstotbnd2  36631  prdsbnd2  36652  isprrngo  36907  isopos  38039  isatl  38158  isnacs3  41434  nacsfix  41436  mzpclall  41451  dnnumch1  41772  dnwech  41776  aomclem3  41784  aomclem8  41789  dfac11  41790  islmodfg  41797  oaordnr  42032  omnord1  42041  oenord1  42052  cantnfresb  42060  rfovcnvf1od  42741  ismnu  43006  sblpnf  43055  rusbcALT  43184  choicefi  43885  climsuselem1  44310  climsuse  44311  cncfuni  44589  dvnprodlem1  44649  stoweidlem31  44734  stoweidlem59  44762  fourierdlem46  44855  fourierdlem62  44871  fourierdlem72  44881  fourierdlem79  44888  fourierdlem88  44897  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem112  44921  qndenserrnbllem  44997  ioorrnopnlem  45007  ioorrnopn  45008  ioorrnopnxr  45010  issal  45017  subsaliuncllem  45060  subsaliuncl  45061  subsalsal  45062  sge0tsms  45083  sge0iunmpt  45121  sge0seq  45149  ovnsubaddlem1  45273  ovnsubaddlem2  45274  hoidmvlelem3  45300  hoidmvlelem4  45301  rrnmbl  45317  hoiqssbllem3  45327  hspmbl  45332  hoimbl  45334  issmflem  45430  issmfd  45438  issmfdf  45440  smfpimltmpt  45449  issmfled  45460  smfpimltxrmptf  45461  smfmbfcex  45463  issmfgtd  45464  smflimlem1  45474  smflimlem2  45475  smflimlem3  45476  smflimlem6  45479  smfpimgtmpt  45484  smfpimgtxrmptf  45487  smfres  45493  smfpimcclem  45510  smfpimcc  45511  dfateq12d  45821  ismgmd  46533  iscllaw  46586  islininds  47081  funcf2lem  47592  isthincd2lem2  47610