Theorem eleq12d 2838

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  neleq12d  3057  cbvraldva2  3356  cbvrexdva2OLD  3358  cdeqel  3798  ruOLD  3803  sbceqbid  3811  cbvrabcsfw  3965  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  sbcel12  4434  elvvuni  5776  elrnmpt1  5983  canth  7401  onnseq  8400  smoeq  8406  smores  8408  smores2  8410  iordsmo  8413  tz7.49  8501  nnaordr  8676  omsmolem  8713  naddel2  8744  fvixp  8960  cbvixp  8972  cbvixpv  8973  mptelixpg  8993  boxcutc  8999  ixpiunwdom  9659  elirr  9666  cantnflt  9741  oemapvali  9753  cantnflem1  9758  cantnf  9762  wemapwe  9766  cnfcom3lem  9772  ttrcltr  9785  rnttrcl  9791  infxpen  10083  dfac8alem  10098  dfac8clem  10101  ac5num  10105  acni2  10115  numacn  10118  acndom  10120  aceq3lem  10189  dfac5  10198  dfac9  10206  dfac13  10212  fin2i  10364  isfin2-2  10388  fin23lem27  10397  isfin3ds  10398  fin23lem17  10407  fin23lem39  10419  isf33lem  10435  isf34lem7  10448  isf34lem6  10449  fin1a2lem10  10478  fin1a2lem12  10480  hsmexlem4  10498  axcc2lem  10505  axcc3  10507  domtriomlem  10511  axdc2lem  10517  axdc3lem2  10520  axdc3lem3  10521  axdc3lem4  10522  axdc3  10523  axdc4lem  10524  axcclem  10526  ac6num  10548  ac6c4  10550  iundom2g  10609  fpwwe2  10712  pwfseqlem1  10727  pwfseqlem4a  10730  pwfseqlem4  10731  ltapi  10972  ltmpi  10973  eluzaddOLD  12938  fzsubel  13620  elfzp1b  13661  axdc4uzlem  14034  wrd2ind  14771  smuval  16527  prdsbasprj  17532  xpsfrnel  17622  ismri2dad  17695  mreexd  17700  mreacs  17716  iscat  17730  iscatd  17731  iscatd2  17739  catcocl  17743  catpropd  17767  brssc  17875  issubc  17899  subcidcl  17908  subccocl  17909  isfunc  17928  isfuncd  17929  cofucl  17952  funcres2b  17961  fuciso  18045  yonedalem3  18350  yonffthlem  18352  ismgm  18679  ismgmd  18690  issstrmgm  18691  issgrpd  18768  ismndd  18794  eqgfval  19216  efgsdm  19772  efgsdmi  19774  efgsrel  19776  efgsp1  19779  efgsres  19780  dprdfcl  20057  ablfaclem3  20131  isdrngd  20787  isdrngdOLD  20789  issrng  20867  issrngd  20878  islmodd  20886  islbs  21098  lbsind  21102  lbspropd  21121  islbs2  21179  lbsextlem4  21186  lbsextg  21187  pzriprnglem8  21522  zndvds  21591  isphl  21669  isphld  21695  phlpropd  21696  frlmlbs  21840  islindf  21855  islinds2  21856  lindfind  21859  lindsind  21860  lindsind2  21862  lindfrn  21864  lindfmm  21870  lsslindf  21873  mhppwdeg  22177  mat1dimmul  22503  istps  22961  tpspropd  22965  eltpsg  22970  eltpsgOLD  22971  islp  23169  1stcelcls  23490  kgeni  23566  kgencn2  23586  ptpjpre1  23600  elptr2  23603  ptbasin  23606  ptbasfi  23610  ptpjcn  23640  ptpjopn  23641  ptcld  23642  ptcldmpt  23643  ptclsg  23644  ptcnp  23651  qtopval  23724  ptcmplem2  24082  ptcmplem3  24083  ptcmplem4  24084  istmd  24103  istgp  24106  tmdgsum  24124  istlm  24214  isusp  24291  prdsdsf  24398  prdsxmet  24400  isms  24480  mspropd  24505  setsxms  24512  setsms  24513  tmsxms  24520  tmsms  24521  isnrg  24702  tngnrg  24716  bcthlem2  25378  bcthlem3  25379  bcthlem4  25380  bcthlem5  25381  iscms  25398  cmspropd  25402  cmssmscld  25403  cmsss  25404  shft2rab  25562  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2lem5  25575  vitalilem2  25663  vitalilem3  25664  vitali  25667  limcfval  25927  limcmpt2  25939  limcres  25941  cnplimc  25942  cnlimci  25944  elcpn  25990  uc1pval  26199  ig1pcl  26238  jensen  27050  axtgcont  28495  tglngval  28577  ishlg  28628  mirbtwnb  28698  trgcopy  28830  trgcopyeu  28832  acopyeu  28860  isinagd  28865  tgasa1  28884  wlkp1lem3  29711  umgrwwlks2on  29990  clwwlknon1  30129  clwwlknonclwlknonf1o  30394  imsmet  30723  smcn  30730  iscbn  30896  sbceqbidf  32515  fnpreimac  32689  isslmd  33181  0nellinds  33363  lindssn  33371  lindfpropd  33375  elrspunidl  33421  lbslsat  33629  lindsunlem  33637  brfldext  33660  submateq  33755  lmatcl  33762  ispcmp  33803  zarcmplem  33827  zhmnrg  33913  ismntoplly  33971  sigapildsys  34126  fiunelcarsg  34281  eulerpartlemgvv  34341  eulerpart  34347  ptpconn  35201  cvmscbv  35226  cvmshmeo  35239  cvmsss2  35242  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift2lem11  35281  cvmlift2lem12  35282  satffunlem1lem1  35370  satffunlem2lem1  35372  sategoelfvb  35387  prv1n  35399  elmpps  35541  cbvriotavw2  36202  cbvmpovw2  36208  cbvmpo1vw2  36209  cbvmpo2vw2  36210  cbvixpvw2  36211  cbvitgvw2  36214  cbvsbcdavw2  36224  cbvixpdavw  36244  cbvrmodavw2  36249  cbvreudavw2  36250  cbvmpodavw2  36257  cbvmpo1davw2  36258  cbvmpo2davw2  36259  cbvixpdavw2  36260  cbvproddavw2  36262  cbvitgdavw2  36263  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  bj-elabd2ALT  36891  bj-ru1  36909  currysetlem  36911  currysetlem1  36913  bj-ismoore  37071  csbfinxpg  37354  pibt2  37383  lindsadd  37573  lindsenlbs  37575  ptrest  37579  upixp  37689  sdclem1  37703  sstotbnd2  37734  prdsbnd2  37755  isprrngo  38010  isopos  39136  isatl  39255  aks6d1c1p6  42071  isnacs3  42666  nacsfix  42668  mzpclall  42683  dnnumch1  43001  dnwech  43005  aomclem3  43013  aomclem8  43018  dfac11  43019  islmodfg  43026  oaordnr  43258  omnord1  43267  oenord1  43278  cantnfresb  43286  rfovcnvf1od  43966  ismnu  44230  sblpnf  44279  rusbcALT  44408  cbvrabv2w  45030  choicefi  45107  climsuselem1  45528  climsuse  45529  cncfuni  45807  dvnprodlem1  45867  stoweidlem31  45952  stoweidlem59  45980  fourierdlem46  46073  fourierdlem62  46089  fourierdlem72  46099  fourierdlem79  46106  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem112  46139  qndenserrnbllem  46215  ioorrnopnlem  46225  ioorrnopn  46226  ioorrnopnxr  46228  issal  46235  subsaliuncllem  46278  subsaliuncl  46279  subsalsal  46280  sge0tsms  46301  sge0iunmpt  46339  sge0seq  46367  ovnsubaddlem1  46491  ovnsubaddlem2  46492  hoidmvlelem3  46518  hoidmvlelem4  46519  rrnmbl  46535  hoiqssbllem3  46545  hspmbl  46550  hoimbl  46552  issmflem  46648  issmfd  46656  issmfdf  46658  smfpimltmpt  46667  issmfled  46678  smfpimltxrmptf  46679  smfmbfcex  46681  issmfgtd  46682  smflimlem1  46692  smflimlem2  46693  smflimlem3  46694  smflimlem6  46697  smfpimgtmpt  46702  smfpimgtxrmptf  46705  smfres  46711  smfpimcclem  46728  smfpimcc  46729  dfateq12d  47041  iscllaw  47912  islininds  48175  funcf2lem  48685  isthincd2lem2  48703