Theorem eleq12d 2835

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  neleq12d  3045  cbvraldva2  3317  cdeqel  3719  ruOLD  3724  sbceqbid  3732  cbvrabcsfw  3874  cbvralcsf  3875  cbvreucsf  3877  cbvrabcsf  3878  sbcel12  4342  elvvuni  5698  elrnmpt1  5909  canth  7314  onnseq  8278  smoeq  8284  smores  8286  smores2  8288  iordsmo  8291  tz7.49  8378  nnaordr  8550  omsmolem  8587  naddel2  8618  fvixp  8844  cbvixp  8856  cbvixpv  8857  mptelixpg  8877  boxcutc  8883  ixpiunwdom  9499  elirr  9509  cantnflt  9588  oemapvali  9600  cantnflem1  9605  cantnf  9609  wemapwe  9613  cnfcom3lem  9619  ttrcltr  9632  rnttrcl  9638  infxpen  9931  dfac8alem  9946  dfac8clem  9949  ac5num  9953  acni2  9963  numacn  9966  acndom  9968  aceq3lem  10037  dfac5  10046  dfac9  10054  dfac13  10060  fin2i  10212  isfin2-2  10236  fin23lem27  10245  isfin3ds  10246  fin23lem17  10255  fin23lem39  10267  isf33lem  10283  isf34lem7  10296  isf34lem6  10297  fin1a2lem10  10326  fin1a2lem12  10328  hsmexlem4  10346  axcc2lem  10353  axcc3  10355  domtriomlem  10359  axdc2lem  10365  axdc3lem2  10368  axdc3lem3  10369  axdc3lem4  10370  axdc3  10371  axdc4lem  10372  axcclem  10374  ac6num  10396  ac6c4  10398  iundom2g  10457  fpwwe2  10561  pwfseqlem1  10576  pwfseqlem4a  10579  pwfseqlem4  10580  ltapi  10821  ltmpi  10822  fzsubel  13509  elfzp1b  13550  axdc4uzlem  13940  wrd2ind  14680  smuval  16445  prdsbasprj  17430  xpsfrnel  17521  ismri2dad  17598  mreexd  17603  mreacs  17619  iscat  17633  iscatd  17634  iscatd2  17642  catcocl  17646  catpropd  17670  brssc  17776  issubc  17797  subcidcl  17806  subccocl  17807  isfunc  17826  isfuncd  17827  cofucl  17850  funcres2b  17859  fuciso  17940  yonedalem3  18241  yonffthlem  18243  ismgm  18604  ismgmd  18615  issstrmgm  18616  issgrpd  18693  ismndd  18719  eqgfval  19146  efgsdm  19700  efgsdmi  19702  efgsrel  19704  efgsp1  19707  efgsres  19708  dprdfcl  19985  ablfaclem3  20059  isdrngd  20741  isdrngdOLD  20743  issrng  20820  issrngd  20831  islmodd  20860  islbs  21070  lbsind  21074  lbspropd  21093  islbs2  21151  lbsextlem4  21158  lbsextg  21159  pzriprnglem8  21467  zndvds  21528  isphl  21607  isphld  21633  phlpropd  21634  frlmlbs  21776  islindf  21791  islinds2  21792  lindfind  21795  lindsind  21796  lindsind2  21798  lindfrn  21800  lindfmm  21806  lsslindf  21809  mhppwdeg  22142  mat1dimmul  22463  istps  22921  tpspropd  22925  eltpsg  22930  islp  23127  1stcelcls  23448  kgeni  23524  kgencn2  23544  ptpjpre1  23558  elptr2  23561  ptbasin  23564  ptbasfi  23568  ptpjcn  23598  ptpjopn  23599  ptcld  23600  ptcldmpt  23601  ptclsg  23602  ptcnp  23609  qtopval  23682  ptcmplem2  24040  ptcmplem3  24041  ptcmplem4  24042  istmd  24061  istgp  24064  tmdgsum  24082  istlm  24172  isusp  24248  prdsdsf  24354  prdsxmet  24356  isms  24436  mspropd  24461  setsxms  24466  setsms  24467  tmsxms  24473  tmsms  24474  isnrg  24647  tngnrg  24661  bcthlem2  25314  bcthlem3  25315  bcthlem4  25316  bcthlem5  25317  iscms  25334  cmspropd  25338  cmssmscld  25339  cmsss  25340  shft2rab  25497  ovolicc2lem3  25508  ovolicc2lem4  25509  ovolicc2lem5  25510  vitalilem2  25598  vitalilem3  25599  vitali  25602  limcfval  25861  limcmpt2  25873  limcres  25875  cnplimc  25876  cnlimci  25878  elcpn  25923  uc1pval  26127  ig1pcl  26166  jensen  26974  axtgcont  28559  tglngval  28641  ishlg  28692  mirbtwnb  28762  trgcopy  28894  trgcopyeu  28896  acopyeu  28924  isinagd  28929  tgasa1  28948  wlkp1lem3  29764  usgrwwlks2on  30048  umgrwwlks2on  30049  clwwlknon1  30189  clwwlknonclwlknonf1o  30454  imsmet  30784  smcn  30791  iscbn  30957  sbceqbidf  32578  fnpreimac  32766  isslmd  33287  0nellinds  33457  lindssn  33465  lindfpropd  33469  elrspunidl  33515  lbslsat  33812  lindsunlem  33820  brfldext  33841  submateq  34005  lmatcl  34012  ispcmp  34053  zarcmplem  34077  zhmnrg  34161  ismntoplly  34221  sigapildsys  34358  fiunelcarsg  34512  eulerpartlemgvv  34572  eulerpart  34578  fineqvinfep  35321  onvf1odlem2  35347  ptpconn  35476  cvmscbv  35501  cvmshmeo  35514  cvmsss2  35517  cvmliftlem7  35534  cvmliftlem10  35537  cvmlift2lem11  35556  cvmlift2lem12  35557  satffunlem1lem1  35645  satffunlem2lem1  35647  sategoelfvb  35662  prv1n  35674  elmpps  35816  cbvriotavw2  36479  cbvmpovw2  36485  cbvmpo1vw2  36486  cbvmpo2vw2  36487  cbvixpvw2  36488  cbvitgvw2  36491  cbvsbcdavw2  36501  cbvixpdavw  36521  cbvrmodavw2  36526  cbvreudavw2  36527  cbvmpodavw2  36534  cbvmpo1davw2  36535  cbvmpo2davw2  36536  cbvixpdavw2  36537  cbvproddavw2  36539  cbvitgdavw2  36540  weiunpo  36708  weiunso  36709  weiunfr  36710  weiunse  36711  bj-elabd2ALT  37293  bj-ru1  37311  currysetlem  37313  currysetlem1  37315  bj-ismoore  37478  csbfinxpg  37765  pibt2  37794  lindsadd  37995  lindsenlbs  37997  ptrest  38001  upixp  38111  sdclem1  38125  sstotbnd2  38156  prdsbnd2  38177  isprrngo  38432  isopos  39687  isatl  39806  aks6d1c1p6  42614  isnacs3  43174  nacsfix  43176  mzpclall  43191  dnnumch1  43504  dnwech  43508  aomclem3  43516  aomclem8  43521  dfac11  43522  islmodfg  43529  oaordnr  43756  omnord1  43765  oenord1  43776  cantnfresb  43784  rfovcnvf1od  44463  ismnu  44720  sblpnf  44769  rusbcALT  44897  cbvrabv2w  45589  choicefi  45660  climsuselem1  46066  climsuse  46067  cncfuni  46343  dvnprodlem1  46403  stoweidlem31  46488  stoweidlem59  46516  fourierdlem46  46609  fourierdlem62  46625  fourierdlem72  46635  fourierdlem79  46642  fourierdlem88  46651  fourierdlem89  46652  fourierdlem90  46653  fourierdlem91  46654  fourierdlem112  46675  qndenserrnbllem  46751  ioorrnopnlem  46761  ioorrnopn  46762  ioorrnopnxr  46764  issal  46771  subsaliuncllem  46814  subsaliuncl  46815  subsalsal  46816  sge0tsms  46837  sge0iunmpt  46875  sge0seq  46903  ovnsubaddlem1  47027  ovnsubaddlem2  47028  hoidmvlelem3  47054  hoidmvlelem4  47055  rrnmbl  47071  hoiqssbllem3  47081  hspmbl  47086  hoimbl  47088  issmflem  47184  issmfd  47192  issmfdf  47194  smfpimltmpt  47203  issmfled  47214  smfpimltxrmptf  47215  smfmbfcex  47217  issmfgtd  47218  smflimlem1  47228  smflimlem2  47229  smflimlem3  47230  smflimlem6  47233  smfpimgtmpt  47238  smfpimgtxrmptf  47241  smfres  47247  smfpimcclem  47264  smfpimcc  47265  dfateq12d  47603  iscllaw  48694  islininds  48951  brab2ddw  49333  brab2ddw2  49334  funcf2lem  49585  isthincd2lem2  49939  setc1onsubc  50106