Theorem eleq12d 2825

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  neleq12d  3037  cbvraldva2  3314  cdeqel  3735  ruOLD  3740  sbceqbid  3748  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  sbcel12  4361  elvvuni  5693  elrnmpt1  5900  canth  7300  onnseq  8264  smoeq  8270  smores  8272  smores2  8274  iordsmo  8277  tz7.49  8364  nnaordr  8535  omsmolem  8572  naddel2  8603  fvixp  8826  cbvixp  8838  cbvixpv  8839  mptelixpg  8859  boxcutc  8865  ixpiunwdom  9476  elirr  9485  cantnflt  9562  oemapvali  9574  cantnflem1  9579  cantnf  9583  wemapwe  9587  cnfcom3lem  9593  ttrcltr  9606  rnttrcl  9612  infxpen  9905  dfac8alem  9920  dfac8clem  9923  ac5num  9927  acni2  9937  numacn  9940  acndom  9942  aceq3lem  10011  dfac5  10020  dfac9  10028  dfac13  10034  fin2i  10186  isfin2-2  10210  fin23lem27  10219  isfin3ds  10220  fin23lem17  10229  fin23lem39  10241  isf33lem  10257  isf34lem7  10270  isf34lem6  10271  fin1a2lem10  10300  fin1a2lem12  10302  hsmexlem4  10320  axcc2lem  10327  axcc3  10329  domtriomlem  10333  axdc2lem  10339  axdc3lem2  10342  axdc3lem3  10343  axdc3lem4  10344  axdc3  10345  axdc4lem  10346  axcclem  10348  ac6num  10370  ac6c4  10372  iundom2g  10431  fpwwe2  10534  pwfseqlem1  10549  pwfseqlem4a  10552  pwfseqlem4  10553  ltapi  10794  ltmpi  10795  eluzaddOLD  12767  fzsubel  13460  elfzp1b  13501  axdc4uzlem  13890  wrd2ind  14630  smuval  16392  prdsbasprj  17376  xpsfrnel  17466  ismri2dad  17543  mreexd  17548  mreacs  17564  iscat  17578  iscatd  17579  iscatd2  17587  catcocl  17591  catpropd  17615  brssc  17721  issubc  17742  subcidcl  17751  subccocl  17752  isfunc  17771  isfuncd  17772  cofucl  17795  funcres2b  17804  fuciso  17885  yonedalem3  18186  yonffthlem  18188  ismgm  18549  ismgmd  18560  issstrmgm  18561  issgrpd  18638  ismndd  18664  eqgfval  19089  efgsdm  19643  efgsdmi  19645  efgsrel  19647  efgsp1  19650  efgsres  19651  dprdfcl  19928  ablfaclem3  20002  isdrngd  20681  isdrngdOLD  20683  issrng  20760  issrngd  20771  islmodd  20800  islbs  21011  lbsind  21015  lbspropd  21034  islbs2  21092  lbsextlem4  21099  lbsextg  21100  pzriprnglem8  21426  zndvds  21487  isphl  21566  isphld  21592  phlpropd  21593  frlmlbs  21735  islindf  21750  islinds2  21751  lindfind  21754  lindsind  21755  lindsind2  21757  lindfrn  21759  lindfmm  21765  lsslindf  21768  mhppwdeg  22066  mat1dimmul  22392  istps  22850  tpspropd  22854  eltpsg  22859  islp  23056  1stcelcls  23377  kgeni  23453  kgencn2  23473  ptpjpre1  23487  elptr2  23490  ptbasin  23493  ptbasfi  23497  ptpjcn  23527  ptpjopn  23528  ptcld  23529  ptcldmpt  23530  ptclsg  23531  ptcnp  23538  qtopval  23611  ptcmplem2  23969  ptcmplem3  23970  ptcmplem4  23971  istmd  23990  istgp  23993  tmdgsum  24011  istlm  24101  isusp  24177  prdsdsf  24283  prdsxmet  24285  isms  24365  mspropd  24390  setsxms  24395  setsms  24396  tmsxms  24402  tmsms  24403  isnrg  24576  tngnrg  24590  bcthlem2  25253  bcthlem3  25254  bcthlem4  25255  bcthlem5  25256  iscms  25273  cmspropd  25277  cmssmscld  25278  cmsss  25279  shft2rab  25437  ovolicc2lem3  25448  ovolicc2lem4  25449  ovolicc2lem5  25450  vitalilem2  25538  vitalilem3  25539  vitali  25542  limcfval  25801  limcmpt2  25813  limcres  25815  cnplimc  25816  cnlimci  25818  elcpn  25864  uc1pval  26073  ig1pcl  26112  jensen  26927  axtgcont  28448  tglngval  28530  ishlg  28581  mirbtwnb  28651  trgcopy  28783  trgcopyeu  28785  acopyeu  28813  isinagd  28818  tgasa1  28837  wlkp1lem3  29653  umgrwwlks2on  29936  clwwlknon1  30075  clwwlknonclwlknonf1o  30340  imsmet  30669  smcn  30676  iscbn  30842  sbceqbidf  32464  fnpreimac  32651  isslmd  33169  0nellinds  33333  lindssn  33341  lindfpropd  33345  elrspunidl  33391  lbslsat  33627  lindsunlem  33635  brfldext  33656  submateq  33820  lmatcl  33827  ispcmp  33868  zarcmplem  33892  zhmnrg  33976  ismntoplly  34036  sigapildsys  34173  fiunelcarsg  34327  eulerpartlemgvv  34387  eulerpart  34393  onvf1odlem2  35146  ptpconn  35275  cvmscbv  35300  cvmshmeo  35313  cvmsss2  35316  cvmliftlem7  35333  cvmliftlem10  35336  cvmlift2lem11  35355  cvmlift2lem12  35356  satffunlem1lem1  35444  satffunlem2lem1  35446  sategoelfvb  35461  prv1n  35473  elmpps  35615  cbvriotavw2  36276  cbvmpovw2  36282  cbvmpo1vw2  36283  cbvmpo2vw2  36284  cbvixpvw2  36285  cbvitgvw2  36288  cbvsbcdavw2  36298  cbvixpdavw  36318  cbvrmodavw2  36323  cbvreudavw2  36324  cbvmpodavw2  36331  cbvmpo1davw2  36332  cbvmpo2davw2  36333  cbvixpdavw2  36334  cbvproddavw2  36336  cbvitgdavw2  36337  weiunpo  36505  weiunso  36506  weiunfr  36507  weiunse  36508  bj-elabd2ALT  36965  bj-ru1  36983  currysetlem  36985  currysetlem1  36987  bj-ismoore  37145  csbfinxpg  37428  pibt2  37457  lindsadd  37659  lindsenlbs  37661  ptrest  37665  upixp  37775  sdclem1  37789  sstotbnd2  37820  prdsbnd2  37841  isprrngo  38096  isopos  39225  isatl  39344  aks6d1c1p6  42153  isnacs3  42749  nacsfix  42751  mzpclall  42766  dnnumch1  43083  dnwech  43087  aomclem3  43095  aomclem8  43100  dfac11  43101  islmodfg  43108  oaordnr  43335  omnord1  43344  oenord1  43355  cantnfresb  43363  rfovcnvf1od  44043  ismnu  44300  sblpnf  44349  rusbcALT  44477  cbvrabv2w  45171  choicefi  45243  climsuselem1  45653  climsuse  45654  cncfuni  45930  dvnprodlem1  45990  stoweidlem31  46075  stoweidlem59  46103  fourierdlem46  46196  fourierdlem62  46212  fourierdlem72  46222  fourierdlem79  46229  fourierdlem88  46238  fourierdlem89  46239  fourierdlem90  46240  fourierdlem91  46241  fourierdlem112  46262  qndenserrnbllem  46338  ioorrnopnlem  46348  ioorrnopn  46349  ioorrnopnxr  46351  issal  46358  subsaliuncllem  46401  subsaliuncl  46402  subsalsal  46403  sge0tsms  46424  sge0iunmpt  46462  sge0seq  46490  ovnsubaddlem1  46614  ovnsubaddlem2  46615  hoidmvlelem3  46641  hoidmvlelem4  46642  rrnmbl  46658  hoiqssbllem3  46668  hspmbl  46673  hoimbl  46675  issmflem  46771  issmfd  46779  issmfdf  46781  smfpimltmpt  46790  issmfled  46801  smfpimltxrmptf  46802  smfmbfcex  46804  issmfgtd  46805  smflimlem1  46815  smflimlem2  46816  smflimlem3  46817  smflimlem6  46820  smfpimgtmpt  46825  smfpimgtxrmptf  46828  smfres  46834  smfpimcclem  46851  smfpimcc  46852  dfateq12d  47163  iscllaw  48226  islininds  48484  brab2ddw  48866  brab2ddw2  48867  funcf2lem  49119  isthincd2lem2  49473  setc1onsubc  49640