Theorem eleq12d 2831

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  neleq12d  3042  cbvraldva2  3314  cdeqel  3723  ruOLD  3728  sbceqbid  3736  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  sbcel12  4352  elvvuni  5701  elrnmpt1  5909  canth  7314  onnseq  8277  smoeq  8283  smores  8285  smores2  8287  iordsmo  8290  tz7.49  8377  nnaordr  8549  omsmolem  8586  naddel2  8617  fvixp  8843  cbvixp  8855  cbvixpv  8856  mptelixpg  8876  boxcutc  8882  ixpiunwdom  9498  elirr  9507  cantnflt  9584  oemapvali  9596  cantnflem1  9601  cantnf  9605  wemapwe  9609  cnfcom3lem  9615  ttrcltr  9628  rnttrcl  9634  infxpen  9927  dfac8alem  9942  dfac8clem  9945  ac5num  9949  acni2  9959  numacn  9962  acndom  9964  aceq3lem  10033  dfac5  10042  dfac9  10050  dfac13  10056  fin2i  10208  isfin2-2  10232  fin23lem27  10241  isfin3ds  10242  fin23lem17  10251  fin23lem39  10263  isf33lem  10279  isf34lem7  10292  isf34lem6  10293  fin1a2lem10  10322  fin1a2lem12  10324  hsmexlem4  10342  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3lem4  10366  axdc3  10367  axdc4lem  10368  axcclem  10370  ac6num  10392  ac6c4  10394  iundom2g  10453  fpwwe2  10557  pwfseqlem1  10572  pwfseqlem4a  10575  pwfseqlem4  10576  ltapi  10817  ltmpi  10818  fzsubel  13505  elfzp1b  13546  axdc4uzlem  13936  wrd2ind  14676  smuval  16441  prdsbasprj  17426  xpsfrnel  17517  ismri2dad  17594  mreexd  17599  mreacs  17615  iscat  17629  iscatd  17630  iscatd2  17638  catcocl  17642  catpropd  17666  brssc  17772  issubc  17793  subcidcl  17802  subccocl  17803  isfunc  17822  isfuncd  17823  cofucl  17846  funcres2b  17855  fuciso  17936  yonedalem3  18237  yonffthlem  18239  ismgm  18600  ismgmd  18611  issstrmgm  18612  issgrpd  18689  ismndd  18715  eqgfval  19142  efgsdm  19696  efgsdmi  19698  efgsrel  19700  efgsp1  19703  efgsres  19704  dprdfcl  19981  ablfaclem3  20055  isdrngd  20733  isdrngdOLD  20735  issrng  20812  issrngd  20823  islmodd  20852  islbs  21063  lbsind  21067  lbspropd  21086  islbs2  21144  lbsextlem4  21151  lbsextg  21152  pzriprnglem8  21478  zndvds  21539  isphl  21618  isphld  21644  phlpropd  21645  frlmlbs  21787  islindf  21802  islinds2  21803  lindfind  21806  lindsind  21807  lindsind2  21809  lindfrn  21811  lindfmm  21817  lsslindf  21820  mhppwdeg  22126  mat1dimmul  22451  istps  22909  tpspropd  22913  eltpsg  22918  islp  23115  1stcelcls  23436  kgeni  23512  kgencn2  23532  ptpjpre1  23546  elptr2  23549  ptbasin  23552  ptbasfi  23556  ptpjcn  23586  ptpjopn  23587  ptcld  23588  ptcldmpt  23589  ptclsg  23590  ptcnp  23597  qtopval  23670  ptcmplem2  24028  ptcmplem3  24029  ptcmplem4  24030  istmd  24049  istgp  24052  tmdgsum  24070  istlm  24160  isusp  24236  prdsdsf  24342  prdsxmet  24344  isms  24424  mspropd  24449  setsxms  24454  setsms  24455  tmsxms  24461  tmsms  24462  isnrg  24635  tngnrg  24649  bcthlem2  25302  bcthlem3  25303  bcthlem4  25304  bcthlem5  25305  iscms  25322  cmspropd  25326  cmssmscld  25327  cmsss  25328  shft2rab  25485  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2lem5  25498  vitalilem2  25586  vitalilem3  25587  vitali  25590  limcfval  25849  limcmpt2  25861  limcres  25863  cnplimc  25864  cnlimci  25866  elcpn  25911  uc1pval  26115  ig1pcl  26154  jensen  26966  axtgcont  28551  tglngval  28633  ishlg  28684  mirbtwnb  28754  trgcopy  28886  trgcopyeu  28888  acopyeu  28916  isinagd  28921  tgasa1  28940  wlkp1lem3  29757  usgrwwlks2on  30041  umgrwwlks2on  30042  clwwlknon1  30182  clwwlknonclwlknonf1o  30447  imsmet  30777  smcn  30784  iscbn  30950  sbceqbidf  32571  fnpreimac  32758  isslmd  33278  0nellinds  33445  lindssn  33453  lindfpropd  33457  elrspunidl  33503  lbslsat  33776  lindsunlem  33784  brfldext  33805  submateq  33969  lmatcl  33976  ispcmp  34017  zarcmplem  34041  zhmnrg  34125  ismntoplly  34185  sigapildsys  34322  fiunelcarsg  34476  eulerpartlemgvv  34536  eulerpart  34542  fineqvinfep  35285  onvf1odlem2  35302  ptpconn  35431  cvmscbv  35456  cvmshmeo  35469  cvmsss2  35472  cvmliftlem7  35489  cvmliftlem10  35492  cvmlift2lem11  35511  cvmlift2lem12  35512  satffunlem1lem1  35600  satffunlem2lem1  35602  sategoelfvb  35617  prv1n  35629  elmpps  35771  cbvriotavw2  36434  cbvmpovw2  36440  cbvmpo1vw2  36441  cbvmpo2vw2  36442  cbvixpvw2  36443  cbvitgvw2  36446  cbvsbcdavw2  36456  cbvixpdavw  36476  cbvrmodavw2  36481  cbvreudavw2  36482  cbvmpodavw2  36489  cbvmpo1davw2  36490  cbvmpo2davw2  36491  cbvixpdavw2  36492  cbvproddavw2  36494  cbvitgdavw2  36495  weiunpo  36663  weiunso  36664  weiunfr  36665  weiunse  36666  bj-elabd2ALT  37248  bj-ru1  37266  currysetlem  37268  currysetlem1  37270  bj-ismoore  37433  csbfinxpg  37718  pibt2  37747  lindsadd  37948  lindsenlbs  37950  ptrest  37954  upixp  38064  sdclem1  38078  sstotbnd2  38109  prdsbnd2  38130  isprrngo  38385  isopos  39640  isatl  39759  aks6d1c1p6  42567  isnacs3  43156  nacsfix  43158  mzpclall  43173  dnnumch1  43490  dnwech  43494  aomclem3  43502  aomclem8  43507  dfac11  43508  islmodfg  43515  oaordnr  43742  omnord1  43751  oenord1  43762  cantnfresb  43770  rfovcnvf1od  44449  ismnu  44706  sblpnf  44755  rusbcALT  44883  cbvrabv2w  45576  choicefi  45647  climsuselem1  46055  climsuse  46056  cncfuni  46332  dvnprodlem1  46392  stoweidlem31  46477  stoweidlem59  46505  fourierdlem46  46598  fourierdlem62  46614  fourierdlem72  46624  fourierdlem79  46631  fourierdlem88  46640  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem112  46664  qndenserrnbllem  46740  ioorrnopnlem  46750  ioorrnopn  46751  ioorrnopnxr  46753  issal  46760  subsaliuncllem  46803  subsaliuncl  46804  subsalsal  46805  sge0tsms  46826  sge0iunmpt  46864  sge0seq  46892  ovnsubaddlem1  47016  ovnsubaddlem2  47017  hoidmvlelem3  47043  hoidmvlelem4  47044  rrnmbl  47060  hoiqssbllem3  47070  hspmbl  47075  hoimbl  47077  issmflem  47173  issmfd  47181  issmfdf  47183  smfpimltmpt  47192  issmfled  47203  smfpimltxrmptf  47204  smfmbfcex  47206  issmfgtd  47207  smflimlem1  47217  smflimlem2  47218  smflimlem3  47219  smflimlem6  47222  smfpimgtmpt  47227  smfpimgtxrmptf  47230  smfres  47236  smfpimcclem  47253  smfpimcc  47254  dfateq12d  47586  iscllaw  48677  islininds  48934  brab2ddw  49316  brab2ddw2  49317  funcf2lem  49568  isthincd2lem2  49922  setc1onsubc  50089