Theorem eleq12d 2830

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

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

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 2115  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  neleq12d  3041  cbvraldva2  3318  cdeqel  3734  ruOLD  3739  sbceqbid  3747  cbvrabcsfw  3890  cbvralcsf  3891  cbvreucsf  3893  cbvrabcsf  3894  sbcel12  4363  elvvuni  5701  elrnmpt1  5909  canth  7312  onnseq  8276  smoeq  8282  smores  8284  smores2  8286  iordsmo  8289  tz7.49  8376  nnaordr  8548  omsmolem  8585  naddel2  8616  fvixp  8840  cbvixp  8852  cbvixpv  8853  mptelixpg  8873  boxcutc  8879  ixpiunwdom  9495  elirr  9504  cantnflt  9581  oemapvali  9593  cantnflem1  9598  cantnf  9602  wemapwe  9606  cnfcom3lem  9612  ttrcltr  9625  rnttrcl  9631  infxpen  9924  dfac8alem  9939  dfac8clem  9942  ac5num  9946  acni2  9956  numacn  9959  acndom  9961  aceq3lem  10030  dfac5  10039  dfac9  10047  dfac13  10053  fin2i  10205  isfin2-2  10229  fin23lem27  10238  isfin3ds  10239  fin23lem17  10248  fin23lem39  10260  isf33lem  10276  isf34lem7  10289  isf34lem6  10290  fin1a2lem10  10319  fin1a2lem12  10321  hsmexlem4  10339  axcc2lem  10346  axcc3  10348  domtriomlem  10352  axdc2lem  10358  axdc3lem2  10361  axdc3lem3  10362  axdc3lem4  10363  axdc3  10364  axdc4lem  10365  axcclem  10367  ac6num  10389  ac6c4  10391  iundom2g  10450  fpwwe2  10554  pwfseqlem1  10569  pwfseqlem4a  10572  pwfseqlem4  10573  ltapi  10814  ltmpi  10815  fzsubel  13476  elfzp1b  13517  axdc4uzlem  13906  wrd2ind  14646  smuval  16408  prdsbasprj  17392  xpsfrnel  17483  ismri2dad  17560  mreexd  17565  mreacs  17581  iscat  17595  iscatd  17596  iscatd2  17604  catcocl  17608  catpropd  17632  brssc  17738  issubc  17759  subcidcl  17768  subccocl  17769  isfunc  17788  isfuncd  17789  cofucl  17812  funcres2b  17821  fuciso  17902  yonedalem3  18203  yonffthlem  18205  ismgm  18566  ismgmd  18577  issstrmgm  18578  issgrpd  18655  ismndd  18681  eqgfval  19105  efgsdm  19659  efgsdmi  19661  efgsrel  19663  efgsp1  19666  efgsres  19667  dprdfcl  19944  ablfaclem3  20018  isdrngd  20698  isdrngdOLD  20700  issrng  20777  issrngd  20788  islmodd  20817  islbs  21028  lbsind  21032  lbspropd  21051  islbs2  21109  lbsextlem4  21116  lbsextg  21117  pzriprnglem8  21443  zndvds  21504  isphl  21583  isphld  21609  phlpropd  21610  frlmlbs  21752  islindf  21767  islinds2  21768  lindfind  21771  lindsind  21772  lindsind2  21774  lindfrn  21776  lindfmm  21782  lsslindf  21785  mhppwdeg  22093  mat1dimmul  22420  istps  22878  tpspropd  22882  eltpsg  22887  islp  23084  1stcelcls  23405  kgeni  23481  kgencn2  23501  ptpjpre1  23515  elptr2  23518  ptbasin  23521  ptbasfi  23525  ptpjcn  23555  ptpjopn  23556  ptcld  23557  ptcldmpt  23558  ptclsg  23559  ptcnp  23566  qtopval  23639  ptcmplem2  23997  ptcmplem3  23998  ptcmplem4  23999  istmd  24018  istgp  24021  tmdgsum  24039  istlm  24129  isusp  24205  prdsdsf  24311  prdsxmet  24313  isms  24393  mspropd  24418  setsxms  24423  setsms  24424  tmsxms  24430  tmsms  24431  isnrg  24604  tngnrg  24618  bcthlem2  25281  bcthlem3  25282  bcthlem4  25283  bcthlem5  25284  iscms  25301  cmspropd  25305  cmssmscld  25306  cmsss  25307  shft2rab  25465  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2lem5  25478  vitalilem2  25566  vitalilem3  25567  vitali  25570  limcfval  25829  limcmpt2  25841  limcres  25843  cnplimc  25844  cnlimci  25846  elcpn  25892  uc1pval  26101  ig1pcl  26140  jensen  26955  axtgcont  28541  tglngval  28623  ishlg  28674  mirbtwnb  28744  trgcopy  28876  trgcopyeu  28878  acopyeu  28906  isinagd  28911  tgasa1  28930  wlkp1lem3  29747  usgrwwlks2on  30031  umgrwwlks2on  30032  clwwlknon1  30172  clwwlknonclwlknonf1o  30437  imsmet  30766  smcn  30773  iscbn  30939  sbceqbidf  32561  fnpreimac  32749  isslmd  33284  0nellinds  33451  lindssn  33459  lindfpropd  33463  elrspunidl  33509  lbslsat  33773  lindsunlem  33781  brfldext  33802  submateq  33966  lmatcl  33973  ispcmp  34014  zarcmplem  34038  zhmnrg  34122  ismntoplly  34182  sigapildsys  34319  fiunelcarsg  34473  eulerpartlemgvv  34533  eulerpart  34539  fineqvinfep  35281  onvf1odlem2  35298  ptpconn  35427  cvmscbv  35452  cvmshmeo  35465  cvmsss2  35468  cvmliftlem7  35485  cvmliftlem10  35488  cvmlift2lem11  35507  cvmlift2lem12  35508  satffunlem1lem1  35596  satffunlem2lem1  35598  sategoelfvb  35613  prv1n  35625  elmpps  35767  cbvriotavw2  36430  cbvmpovw2  36436  cbvmpo1vw2  36437  cbvmpo2vw2  36438  cbvixpvw2  36439  cbvitgvw2  36442  cbvsbcdavw2  36452  cbvixpdavw  36472  cbvrmodavw2  36477  cbvreudavw2  36478  cbvmpodavw2  36485  cbvmpo1davw2  36486  cbvmpo2davw2  36487  cbvixpdavw2  36488  cbvproddavw2  36490  cbvitgdavw2  36491  weiunpo  36659  weiunso  36660  weiunfr  36661  weiunse  36662  bj-elabd2ALT  37126  bj-ru1  37144  currysetlem  37146  currysetlem1  37148  bj-ismoore  37310  csbfinxpg  37593  pibt2  37622  lindsadd  37814  lindsenlbs  37816  ptrest  37820  upixp  37930  sdclem1  37944  sstotbnd2  37975  prdsbnd2  37996  isprrngo  38251  isopos  39440  isatl  39559  aks6d1c1p6  42368  isnacs3  42952  nacsfix  42954  mzpclall  42969  dnnumch1  43286  dnwech  43290  aomclem3  43298  aomclem8  43303  dfac11  43304  islmodfg  43311  oaordnr  43538  omnord1  43547  oenord1  43558  cantnfresb  43566  rfovcnvf1od  44245  ismnu  44502  sblpnf  44551  rusbcALT  44679  cbvrabv2w  45372  choicefi  45444  climsuselem1  45853  climsuse  45854  cncfuni  46130  dvnprodlem1  46190  stoweidlem31  46275  stoweidlem59  46303  fourierdlem46  46396  fourierdlem62  46412  fourierdlem72  46422  fourierdlem79  46429  fourierdlem88  46438  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem112  46462  qndenserrnbllem  46538  ioorrnopnlem  46548  ioorrnopn  46549  ioorrnopnxr  46551  issal  46558  subsaliuncllem  46601  subsaliuncl  46602  subsalsal  46603  sge0tsms  46624  sge0iunmpt  46662  sge0seq  46690  ovnsubaddlem1  46814  ovnsubaddlem2  46815  hoidmvlelem3  46841  hoidmvlelem4  46842  rrnmbl  46858  hoiqssbllem3  46868  hspmbl  46873  hoimbl  46875  issmflem  46971  issmfd  46979  issmfdf  46981  smfpimltmpt  46990  issmfled  47001  smfpimltxrmptf  47002  smfmbfcex  47004  issmfgtd  47005  smflimlem1  47015  smflimlem2  47016  smflimlem3  47017  smflimlem6  47020  smfpimgtmpt  47025  smfpimgtxrmptf  47028  smfres  47034  smfpimcclem  47051  smfpimcc  47052  dfateq12d  47372  iscllaw  48435  islininds  48692  brab2ddw  49074  brab2ddw2  49075  funcf2lem  49326  isthincd2lem2  49680  setc1onsubc  49847