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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729  df-clel 2815

This theorem is referenced by:  neleq12d  3051  cbvraldva2  3320  cbvrexdva2OLD  3322  cdeqel  3721  ru  3725  sbceqbid  3733  cbvrabcsfw  3886  cbvralcsf  3887  cbvreucsf  3889  cbvrabcsf  3890  sbcel12  4353  elvvuni  5682  elrnmpt1  5887  canth  7271  onnseq  8224  smoeq  8230  smores  8232  smores2  8234  iordsmo  8237  tz7.49  8325  nnaordr  8501  omsmolem  8537  fvixp  8740  cbvixp  8752  mptelixpg  8773  boxcutc  8779  ixpiunwdom  9426  elirr  9433  cantnflt  9508  oemapvali  9520  cantnflem1  9525  cantnf  9529  wemapwe  9533  cnfcom3lem  9539  ttrcltr  9552  rnttrcl  9558  infxpen  9850  dfac8alem  9865  dfac8clem  9868  ac5num  9872  acni2  9882  numacn  9885  acndom  9887  aceq3lem  9956  dfac5  9964  dfac9  9972  dfac13  9978  fin2i  10131  isfin2-2  10155  fin23lem27  10164  isfin3ds  10165  fin23lem17  10174  fin23lem39  10186  isf33lem  10202  isf34lem7  10215  isf34lem6  10216  fin1a2lem10  10245  fin1a2lem12  10247  hsmexlem4  10265  axcc2lem  10272  axcc3  10274  domtriomlem  10278  axdc2lem  10284  axdc3lem2  10287  axdc3lem3  10288  axdc3lem4  10289  axdc3  10290  axdc4lem  10291  axcclem  10293  ac6num  10315  ac6c4  10317  iundom2g  10376  fpwwe2  10479  pwfseqlem1  10494  pwfseqlem4a  10497  pwfseqlem4  10498  ltapi  10739  ltmpi  10740  eluzadd  12693  fzsubel  13372  elfzp1b  13413  axdc4uzlem  13783  wrd2ind  14515  smuval  16267  prdsbasprj  17260  xpsfrnel  17350  ismri2dad  17423  mreexd  17428  mreacs  17444  iscat  17458  iscatd  17459  iscatd2  17467  catcocl  17471  catpropd  17495  brssc  17603  issubc  17627  subcidcl  17636  subccocl  17637  isfunc  17656  isfuncd  17657  cofucl  17680  funcres2b  17689  fuciso  17770  yonedalem3  18075  yonffthlem  18077  ismgm  18404  issstrmgm  18414  ismndd  18484  eqgfval  18880  efgsdm  19411  efgsdmi  19413  efgsrel  19415  efgsp1  19418  efgsres  19419  dprdfcl  19691  ablfaclem3  19765  isdrngd  20098  issrng  20193  issrngd  20204  islmodd  20212  islbs  20421  lbsind  20425  lbspropd  20444  islbs2  20499  lbsextlem4  20506  lbsextg  20507  zndvds  20840  isphl  20916  isphld  20942  phlpropd  20943  frlmlbs  21087  islindf  21102  islinds2  21103  lindfind  21106  lindsind  21107  lindsind2  21109  lindfrn  21111  lindfmm  21117  lsslindf  21120  mhppwdeg  21423  mat1dimmul  21708  istps  22166  tpspropd  22170  eltpsg  22175  eltpsgOLD  22176  islp  22374  1stcelcls  22695  kgeni  22771  kgencn2  22791  ptpjpre1  22805  elptr2  22808  ptbasin  22811  ptbasfi  22815  ptpjcn  22845  ptpjopn  22846  ptcld  22847  ptcldmpt  22848  ptclsg  22849  ptcnp  22856  qtopval  22929  ptcmplem2  23287  ptcmplem3  23288  ptcmplem4  23289  istmd  23308  istgp  23311  tmdgsum  23329  istlm  23419  isusp  23496  prdsdsf  23603  prdsxmet  23605  isms  23685  mspropd  23710  setsxms  23717  setsms  23718  tmsxms  23725  tmsms  23726  isnrg  23907  tngnrg  23921  bcthlem2  24572  bcthlem3  24573  bcthlem4  24574  bcthlem5  24575  iscms  24592  cmspropd  24596  cmssmscld  24597  cmsss  24598  shft2rab  24755  ovolicc2lem3  24766  ovolicc2lem4  24767  ovolicc2lem5  24768  vitalilem2  24856  vitalilem3  24857  vitali  24860  limcfval  25119  limcmpt2  25131  limcres  25133  cnplimc  25134  cnlimci  25136  elcpn  25181  uc1pval  25387  ig1pcl  25423  jensen  26221  axtgcont  26966  tglngval  27048  ishlg  27099  mirbtwnb  27169  trgcopy  27301  trgcopyeu  27303  acopyeu  27331  isinagd  27336  tgasa1  27355  wlkp1lem3  28179  umgrwwlks2on  28458  clwwlknon1  28597  clwwlknonclwlknonf1o  28862  imsmet  29189  smcn  29196  iscbn  29362  sbceqbidf  30971  fnpreimac  31143  isslmd  31590  0nellinds  31705  lindssn  31712  lindfpropd  31715  elrspunidl  31745  lbslsat  31839  lindsunlem  31845  brfldext  31862  submateq  31899  lmatcl  31906  ispcmp  31947  zarcmplem  31971  zhmnrg  32057  ismntoplly  32115  sigapildsys  32270  fiunelcarsg  32423  eulerpartlemgvv  32483  eulerpart  32489  ptpconn  33334  cvmscbv  33359  cvmshmeo  33372  cvmsss2  33375  cvmliftlem7  33392  cvmliftlem10  33395  cvmlift2lem11  33414  cvmlift2lem12  33415  satffunlem1lem1  33503  satffunlem2lem1  33505  sategoelfvb  33520  prv1n  33532  elmpps  33674  naddel2  33967  bj-elabd2ALT  35186  currysetlem  35207  currysetlem1  35209  bj-ismoore  35348  csbfinxpg  35631  pibt2  35660  lindsadd  35842  lindsenlbs  35844  ptrest  35848  upixp  35959  sdclem1  35973  sstotbnd2  36004  prdsbnd2  36025  isprrngo  36280  isopos  37414  isatl  37533  isnacs3  40748  nacsfix  40750  mzpclall  40765  dnnumch1  41086  dnwech  41090  aomclem3  41098  aomclem8  41103  dfac11  41104  islmodfg  41111  rfovcnvf1od  41846  ismnu  42113  sblpnf  42162  rusbcALT  42291  choicefi  42981  climsuselem1  43398  climsuse  43399  cncfuni  43677  dvnprodlem1  43737  stoweidlem31  43822  stoweidlem59  43850  fourierdlem46  43943  fourierdlem62  43959  fourierdlem72  43969  fourierdlem79  43976  fourierdlem88  43985  fourierdlem89  43986  fourierdlem90  43987  fourierdlem91  43988  fourierdlem112  44009  qndenserrnbllem  44085  ioorrnopnlem  44095  ioorrnopn  44096  ioorrnopnxr  44098  issal  44105  subsaliuncllem  44146  subsaliuncl  44147  subsalsal  44148  sge0tsms  44169  sge0iunmpt  44207  sge0seq  44235  ovnsubaddlem1  44359  ovnsubaddlem2  44360  hoidmvlelem3  44386  hoidmvlelem4  44387  rrnmbl  44403  hoiqssbllem3  44413  hspmbl  44418  hoimbl  44420  issmflem  44516  issmfd  44524  issmfdf  44526  smfpimltmpt  44535  issmfled  44546  smfpimltxrmptf  44547  smfmbfcex  44549  issmfgtd  44550  smflimlem1  44560  smflimlem2  44561  smflimlem3  44562  smflimlem6  44565  smfpimgtmpt  44570  smfpimgtxrmptf  44573  smfres  44579  smfpimcclem  44596  smfpimcc  44597  dfateq12d  44883  ismgmd  45595  iscllaw  45648  islininds  46052  funcf2lem  46564  isthincd2lem2  46582