Theorem eleq12d 2832

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  neleq12d  3048  cbvraldva2  3345  cbvrexdva2OLD  3347  cdeqel  3784  ruOLD  3789  sbceqbid  3797  cbvrabcsfw  3951  cbvralcsf  3952  cbvreucsf  3954  cbvrabcsf  3955  sbcel12  4416  elvvuni  5764  elrnmpt1  5973  canth  7384  onnseq  8382  smoeq  8388  smores  8390  smores2  8392  iordsmo  8395  tz7.49  8483  nnaordr  8656  omsmolem  8693  naddel2  8724  fvixp  8940  cbvixp  8952  cbvixpv  8953  mptelixpg  8973  boxcutc  8979  ixpiunwdom  9627  elirr  9634  cantnflt  9709  oemapvali  9721  cantnflem1  9726  cantnf  9730  wemapwe  9734  cnfcom3lem  9740  ttrcltr  9753  rnttrcl  9759  infxpen  10051  dfac8alem  10066  dfac8clem  10069  ac5num  10073  acni2  10083  numacn  10086  acndom  10088  aceq3lem  10157  dfac5  10166  dfac9  10174  dfac13  10180  fin2i  10332  isfin2-2  10356  fin23lem27  10365  isfin3ds  10366  fin23lem17  10375  fin23lem39  10387  isf33lem  10403  isf34lem7  10416  isf34lem6  10417  fin1a2lem10  10446  fin1a2lem12  10448  hsmexlem4  10466  axcc2lem  10473  axcc3  10475  domtriomlem  10479  axdc2lem  10485  axdc3lem2  10488  axdc3lem3  10489  axdc3lem4  10490  axdc3  10491  axdc4lem  10492  axcclem  10494  ac6num  10516  ac6c4  10518  iundom2g  10577  fpwwe2  10680  pwfseqlem1  10695  pwfseqlem4a  10698  pwfseqlem4  10699  ltapi  10940  ltmpi  10941  eluzaddOLD  12910  fzsubel  13596  elfzp1b  13637  axdc4uzlem  14020  wrd2ind  14757  smuval  16514  prdsbasprj  17518  xpsfrnel  17608  ismri2dad  17681  mreexd  17686  mreacs  17702  iscat  17716  iscatd  17717  iscatd2  17725  catcocl  17729  catpropd  17753  brssc  17861  issubc  17885  subcidcl  17894  subccocl  17895  isfunc  17914  isfuncd  17915  cofucl  17938  funcres2b  17947  fuciso  18031  yonedalem3  18336  yonffthlem  18338  ismgm  18666  ismgmd  18677  issstrmgm  18678  issgrpd  18755  ismndd  18781  eqgfval  19206  efgsdm  19762  efgsdmi  19764  efgsrel  19766  efgsp1  19769  efgsres  19770  dprdfcl  20047  ablfaclem3  20121  isdrngd  20781  isdrngdOLD  20783  issrng  20861  issrngd  20872  islmodd  20880  islbs  21092  lbsind  21096  lbspropd  21115  islbs2  21173  lbsextlem4  21180  lbsextg  21181  pzriprnglem8  21516  zndvds  21585  isphl  21663  isphld  21689  phlpropd  21690  frlmlbs  21834  islindf  21849  islinds2  21850  lindfind  21853  lindsind  21854  lindsind2  21856  lindfrn  21858  lindfmm  21864  lsslindf  21867  mhppwdeg  22171  mat1dimmul  22497  istps  22955  tpspropd  22959  eltpsg  22964  eltpsgOLD  22965  islp  23163  1stcelcls  23484  kgeni  23560  kgencn2  23580  ptpjpre1  23594  elptr2  23597  ptbasin  23600  ptbasfi  23604  ptpjcn  23634  ptpjopn  23635  ptcld  23636  ptcldmpt  23637  ptclsg  23638  ptcnp  23645  qtopval  23718  ptcmplem2  24076  ptcmplem3  24077  ptcmplem4  24078  istmd  24097  istgp  24100  tmdgsum  24118  istlm  24208  isusp  24285  prdsdsf  24392  prdsxmet  24394  isms  24474  mspropd  24499  setsxms  24506  setsms  24507  tmsxms  24514  tmsms  24515  isnrg  24696  tngnrg  24710  bcthlem2  25372  bcthlem3  25373  bcthlem4  25374  bcthlem5  25375  iscms  25392  cmspropd  25396  cmssmscld  25397  cmsss  25398  shft2rab  25556  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2lem5  25569  vitalilem2  25657  vitalilem3  25658  vitali  25661  limcfval  25921  limcmpt2  25933  limcres  25935  cnplimc  25936  cnlimci  25938  elcpn  25984  uc1pval  26193  ig1pcl  26232  jensen  27046  axtgcont  28491  tglngval  28573  ishlg  28624  mirbtwnb  28694  trgcopy  28826  trgcopyeu  28828  acopyeu  28856  isinagd  28861  tgasa1  28880  wlkp1lem3  29707  umgrwwlks2on  29986  clwwlknon1  30125  clwwlknonclwlknonf1o  30390  imsmet  30719  smcn  30726  iscbn  30892  sbceqbidf  32514  fnpreimac  32687  isslmd  33190  0nellinds  33377  lindssn  33385  lindfpropd  33389  elrspunidl  33435  lbslsat  33643  lindsunlem  33651  brfldext  33674  submateq  33769  lmatcl  33776  ispcmp  33817  zarcmplem  33841  zhmnrg  33927  ismntoplly  33987  sigapildsys  34142  fiunelcarsg  34297  eulerpartlemgvv  34357  eulerpart  34363  ptpconn  35217  cvmscbv  35242  cvmshmeo  35255  cvmsss2  35258  cvmliftlem7  35275  cvmliftlem10  35278  cvmlift2lem11  35297  cvmlift2lem12  35298  satffunlem1lem1  35386  satffunlem2lem1  35388  sategoelfvb  35403  prv1n  35415  elmpps  35557  cbvriotavw2  36218  cbvmpovw2  36224  cbvmpo1vw2  36225  cbvmpo2vw2  36226  cbvixpvw2  36227  cbvitgvw2  36230  cbvsbcdavw2  36240  cbvixpdavw  36260  cbvrmodavw2  36265  cbvreudavw2  36266  cbvmpodavw2  36273  cbvmpo1davw2  36274  cbvmpo2davw2  36275  cbvixpdavw2  36276  cbvproddavw2  36278  cbvitgdavw2  36279  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  bj-elabd2ALT  36907  bj-ru1  36925  currysetlem  36927  currysetlem1  36929  bj-ismoore  37087  csbfinxpg  37370  pibt2  37399  lindsadd  37599  lindsenlbs  37601  ptrest  37605  upixp  37715  sdclem1  37729  sstotbnd2  37760  prdsbnd2  37781  isprrngo  38036  isopos  39161  isatl  39280  aks6d1c1p6  42095  isnacs3  42697  nacsfix  42699  mzpclall  42714  dnnumch1  43032  dnwech  43036  aomclem3  43044  aomclem8  43049  dfac11  43050  islmodfg  43057  oaordnr  43285  omnord1  43294  oenord1  43305  cantnfresb  43313  rfovcnvf1od  43993  ismnu  44256  sblpnf  44305  rusbcALT  44434  cbvrabv2w  45067  choicefi  45142  climsuselem1  45562  climsuse  45563  cncfuni  45841  dvnprodlem1  45901  stoweidlem31  45986  stoweidlem59  46014  fourierdlem46  46107  fourierdlem62  46123  fourierdlem72  46133  fourierdlem79  46140  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem112  46173  qndenserrnbllem  46249  ioorrnopnlem  46259  ioorrnopn  46260  ioorrnopnxr  46262  issal  46269  subsaliuncllem  46312  subsaliuncl  46313  subsalsal  46314  sge0tsms  46335  sge0iunmpt  46373  sge0seq  46401  ovnsubaddlem1  46525  ovnsubaddlem2  46526  hoidmvlelem3  46552  hoidmvlelem4  46553  rrnmbl  46569  hoiqssbllem3  46579  hspmbl  46584  hoimbl  46586  issmflem  46682  issmfd  46690  issmfdf  46692  smfpimltmpt  46701  issmfled  46712  smfpimltxrmptf  46713  smfmbfcex  46715  issmfgtd  46716  smflimlem1  46726  smflimlem2  46727  smflimlem3  46728  smflimlem6  46731  smfpimgtmpt  46736  smfpimgtxrmptf  46739  smfres  46745  smfpimcclem  46762  smfpimcc  46763  dfateq12d  47075  iscllaw  48032  islininds  48291  funcf2lem  48810  isthincd2lem2  48835