Theorem eleq12d 2833

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 278	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  neleq12d  3052  cbvraldva2  3381  cbvrexdva2  3382  cdeqel  3706  ru  3710  sbceqbid  3718  cbvrabcsfw  3872  cbvralcsf  3873  cbvreucsf  3875  cbvrabcsf  3876  sbcel12  4339  elvvuni  5654  elrnmpt1  5856  canth  7209  onnseq  8146  smoeq  8152  smores  8154  smores2  8156  iordsmo  8159  tz7.49  8246  nnaordr  8413  omsmolem  8447  fvixp  8648  cbvixp  8660  mptelixpg  8681  boxcutc  8687  ixpiunwdom  9279  elirr  9286  cantnflt  9360  oemapvali  9372  cantnflem1  9377  cantnf  9381  wemapwe  9385  cnfcom3lem  9391  infxpen  9701  dfac8alem  9716  dfac8clem  9719  ac5num  9723  acni2  9733  numacn  9736  acndom  9738  aceq3lem  9807  dfac5  9815  dfac9  9823  dfac13  9829  fin2i  9982  isfin2-2  10006  fin23lem27  10015  isfin3ds  10016  fin23lem17  10025  fin23lem39  10037  isf33lem  10053  isf34lem7  10066  isf34lem6  10067  fin1a2lem10  10096  fin1a2lem12  10098  hsmexlem4  10116  axcc2lem  10123  axcc3  10125  domtriomlem  10129  axdc2lem  10135  axdc3lem2  10138  axdc3lem3  10139  axdc3lem4  10140  axdc3  10141  axdc4lem  10142  axcclem  10144  ac6num  10166  ac6c4  10168  iundom2g  10227  fpwwe2  10330  pwfseqlem1  10345  pwfseqlem4a  10348  pwfseqlem4  10349  ltapi  10590  ltmpi  10591  eluzadd  12542  fzsubel  13221  elfzp1b  13262  axdc4uzlem  13631  wrd2ind  14364  smuval  16116  prdsbasprj  17100  xpsfrnel  17190  ismri2dad  17263  mreexd  17268  mreacs  17284  iscat  17298  iscatd  17299  iscatd2  17307  catcocl  17311  catpropd  17335  brssc  17443  issubc  17466  subcidcl  17475  subccocl  17476  isfunc  17495  isfuncd  17496  cofucl  17519  funcres2b  17528  fuciso  17609  yonedalem3  17914  yonffthlem  17916  ismgm  18242  issstrmgm  18252  ismndd  18322  eqgfval  18719  efgsdm  19251  efgsdmi  19253  efgsrel  19255  efgsp1  19258  efgsres  19259  dprdfcl  19531  ablfaclem3  19605  isdrngd  19931  issrng  20025  issrngd  20036  islmodd  20044  islbs  20253  lbsind  20257  lbspropd  20276  islbs2  20331  lbsextlem4  20338  lbsextg  20339  zndvds  20669  isphl  20745  isphld  20771  phlpropd  20772  frlmlbs  20914  islindf  20929  islinds2  20930  lindfind  20933  lindsind  20934  lindsind2  20936  lindfrn  20938  lindfmm  20944  lsslindf  20947  mhppwdeg  21250  mat1dimmul  21533  istps  21991  tpspropd  21995  eltpsg  22000  eltpsgOLD  22001  islp  22199  1stcelcls  22520  kgeni  22596  kgencn2  22616  ptpjpre1  22630  elptr2  22633  ptbasin  22636  ptbasfi  22640  ptpjcn  22670  ptpjopn  22671  ptcld  22672  ptcldmpt  22673  ptclsg  22674  ptcnp  22681  qtopval  22754  ptcmplem2  23112  ptcmplem3  23113  ptcmplem4  23114  istmd  23133  istgp  23136  tmdgsum  23154  istlm  23244  isusp  23321  prdsdsf  23428  prdsxmet  23430  isms  23510  mspropd  23535  setsxms  23540  setsms  23541  tmsxms  23548  tmsms  23549  isnrg  23730  tngnrg  23744  bcthlem2  24394  bcthlem3  24395  bcthlem4  24396  bcthlem5  24397  iscms  24414  cmspropd  24418  cmssmscld  24419  cmsss  24420  shft2rab  24577  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2lem5  24590  vitalilem2  24678  vitalilem3  24679  vitali  24682  limcfval  24941  limcmpt2  24953  limcres  24955  cnplimc  24956  cnlimci  24958  elcpn  25003  uc1pval  25209  ig1pcl  25245  jensen  26043  axtgcont  26734  tglngval  26816  ishlg  26867  mirbtwnb  26937  trgcopy  27069  trgcopyeu  27071  acopyeu  27099  isinagd  27104  tgasa1  27123  wlkp1lem3  27945  umgrwwlks2on  28223  clwwlknon1  28362  clwwlknonclwlknonf1o  28627  imsmet  28954  smcn  28961  iscbn  29127  sbceqbidf  30736  fnpreimac  30910  isslmd  31357  0nellinds  31468  lindssn  31475  lindfpropd  31478  elrspunidl  31508  lbslsat  31601  lindsunlem  31607  brfldext  31624  submateq  31661  lmatcl  31668  ispcmp  31709  zarcmplem  31733  zhmnrg  31817  ismntoplly  31875  sigapildsys  32030  fiunelcarsg  32183  eulerpartlemgvv  32243  eulerpart  32249  ptpconn  33095  cvmscbv  33120  cvmshmeo  33133  cvmsss2  33136  cvmliftlem7  33153  cvmliftlem10  33156  cvmlift2lem11  33175  cvmlift2lem12  33176  satffunlem1lem1  33264  satffunlem2lem1  33266  sategoelfvb  33281  prv1n  33293  elmpps  33435  ttrcltr  33702  rnttrcl  33708  naddel2  33767  bj-elabd2ALT  35040  currysetlem  35061  currysetlem1  35063  bj-ismoore  35203  csbfinxpg  35486  pibt2  35515  lindsadd  35697  lindsenlbs  35699  ptrest  35703  upixp  35814  sdclem1  35828  sstotbnd2  35859  prdsbnd2  35880  isprrngo  36135  isopos  37121  isatl  37240  isnacs3  40448  nacsfix  40450  mzpclall  40465  dnnumch1  40785  dnwech  40789  aomclem3  40797  aomclem8  40802  dfac11  40803  islmodfg  40810  rfovcnvf1od  41501  ismnu  41768  sblpnf  41817  rusbcALT  41946  choicefi  42629  climsuselem1  43038  climsuse  43039  cncfuni  43317  dvnprodlem1  43377  stoweidlem31  43462  stoweidlem59  43490  fourierdlem46  43583  fourierdlem62  43599  fourierdlem72  43609  fourierdlem79  43616  fourierdlem88  43625  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem112  43649  qndenserrnbllem  43725  ioorrnopnlem  43735  ioorrnopn  43736  ioorrnopnxr  43738  issal  43745  subsaliuncllem  43786  subsaliuncl  43787  subsalsal  43788  sge0tsms  43808  sge0iunmpt  43846  sge0seq  43874  ovnsubaddlem1  43998  ovnsubaddlem2  43999  hoidmvlelem3  44025  hoidmvlelem4  44026  rrnmbl  44042  hoiqssbllem3  44052  hspmbl  44057  hoimbl  44059  issmflem  44150  issmfd  44158  issmfdf  44160  smfpimltmpt  44169  issmfled  44180  smfpimltxrmpt  44181  smfmbfcex  44182  issmfgtd  44183  smflimlem1  44193  smflimlem2  44194  smflimlem3  44195  smflimlem6  44198  smfpimgtmpt  44203  smfpimgtxrmpt  44206  smfres  44211  smfpimcclem  44227  smfpimcc  44228  dfateq12d  44505  ismgmd  45218  iscllaw  45271  islininds  45675  funcf2lem  46187  isthincd2lem2  46205