Theorem eleq12d 2857

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  neleq12d  3069  cbvraldva2  3340  cdeqel  3740  sbceqbid  3752  cbvrabcsfw  3895  cbvralcsf  3896  cbvreucsf  3898  cbvrabcsf  3899  sbcel12  4377  elvvuni  5740  elrnmpt1  5952  canth  7366  onnseq  8332  smoeq  8338  smores  8340  smores2  8342  iordsmo  8345  tz7.49  8433  nnaordr  8607  omsmolem  8644  naddel2  8676  fvixp  8901  cbvixp  8913  cbvixpv  8914  mptelixpg  8934  boxcutc  8940  ixpiunwdom  9553  elirr  9563  cantnflt  9642  oemapvali  9654  cantnflem1  9659  cantnf  9663  wemapwe  9667  cnfcom3lem  9673  ttrcltr  9686  rnttrcl  9692  infxpen  9999  dfac8alem  10014  dfac8clem  10017  ac5num  10021  acni2  10031  numacn  10034  acndom  10036  aceq3lem  10105  dfac5  10113  dfac9  10121  dfac13  10127  fin2i  10280  isfin2-2  10304  fin23lem27  10313  isfin3ds  10314  fin23lem17  10323  fin23lem39  10335  isf33lem  10351  isf34lem7  10364  isf34lem6  10365  fin1a2lem10  10394  fin1a2lem12  10396  hsmexlem4  10414  axcc2lem  10421  axcc3  10423  domtriomlem  10427  axdc2lem  10433  axdc3lem2  10436  axdc3lem3  10437  axdc3lem4  10438  axdc3  10439  axdc4lem  10440  axcclem  10442  ac6num  10464  ac6c4  10466  iundom2g  10525  fpwwe2  10629  pwfseqlem1  10644  pwfseqlem4a  10647  pwfseqlem4  10648  ltapi  10889  ltmpi  10890  fzsubel  13590  elfzp1b  13631  axdc4uzlem  14021  wrd2ind  14762  smuval  16540  prdsbasprj  17526  xpsfrnel  17617  ismri2dad  17694  mreexd  17699  mreacs  17715  iscat  17729  iscatd  17730  iscatd2  17738  catcocl  17742  catpropd  17766  brssc  17872  issubc  17893  subcidcl  17902  subccocl  17903  isfunc  17922  isfuncd  17923  cofucl  17946  funcres2b  17955  fuciso  18036  yonedalem3  18337  yonffthlem  18339  ismgm  18700  ismgmd  18711  issstrmgm  18712  issgrpd  18789  ismndd  18815  eqgfval  19245  efgsdm  19801  efgsdmi  19803  efgsrel  19805  efgsp1  19808  efgsres  19809  dprdfcl  20086  ablfaclem3  20160  isdrngd  20850  isdrngdOLD  20852  issrng  20928  issrngd  20939  islmodd  20968  islbs  21178  lbsind  21182  lbspropd  21201  islbs2  21259  lbsextlem4  21266  lbsextg  21267  pzriprnglem8  21619  zndvds  21680  isphl  21759  isphld  21785  phlpropd  21786  frlmlbs  21928  islindf  21943  islinds2  21944  lindfind  21947  lindsind  21948  lindsind2  21950  lindfrn  21952  lindfmm  21958  lsslindf  21961  mhppwdeg  22294  mat1dimmul  22614  istps  23072  tpspropd  23076  eltpsg  23081  islp  23278  1stcelcls  23599  kgeni  23675  kgencn2  23695  ptpjpre1  23709  elptr2  23712  ptbasin  23715  ptbasfi  23719  ptpjcn  23749  ptpjopn  23750  ptcld  23751  ptcldmpt  23752  ptclsg  23753  ptcnp  23760  qtopval  23833  ptcmplem2  24191  ptcmplem3  24192  ptcmplem4  24193  istmd  24212  istgp  24215  tmdgsum  24233  istlm  24323  isusp  24399  prdsdsf  24505  prdsxmet  24507  isms  24587  mspropd  24612  setsxms  24617  setsms  24618  tmsxms  24624  tmsms  24625  isnrg  24798  tngnrg  24812  bcthlem2  25465  bcthlem3  25466  bcthlem4  25467  bcthlem5  25468  iscms  25485  cmspropd  25489  cmssmscld  25490  cmsss  25491  shft2rab  25648  ovolicc2lem3  25659  ovolicc2lem4  25660  ovolicc2lem5  25661  vitalilem2  25749  vitalilem3  25750  vitali  25753  limcfval  26012  limcmpt2  26024  limcres  26026  cnplimc  26027  cnlimci  26029  elcpn  26074  uc1pval  26278  ig1pcl  26317  jensen  27134  axtgcont  28719  tglngval  28801  ishlg2  28852  ishlg  28855  mirbtwnb  28930  trgcopy  29096  trgcopyeu  29098  acopyeu  29126  isinagd  29137  tgasa1  29156  wlkp1lem3  30004  usgrwwlks2on  30288  umgrwwlks2on  30289  clwwlknon1  30429  clwwlknonclwlknonf1o  30694  imsmet  31024  smcn  31031  iscbn  31197  sbceqbidf  32814  fnpreimac  32996  isslmd  33503  0nellinds  33666  lindssn  33672  lindfpropd  33676  elrspunidl  33717  lbslsat  33987  lindsunlem  33995  brfldext  34016  submateq  34180  lmatcl  34187  ispcmp  34228  zarcmplem  34252  zhmnrg  34336  ismntoplly  34396  sigapildsys  34533  fiunelcarsg  34687  eulerpartlemgvv  34747  eulerpart  34753  fineqvinfep  35519  onvf1odlem2  35569  ptpconn  35706  cvmscbv  35731  cvmshmeo  35744  cvmsss2  35747  cvmliftlem7  35764  cvmliftlem10  35767  cvmlift2lem11  35786  cvmlift2lem12  35787  satffunlem1lem1  35875  satffunlem2lem1  35877  sategoelfvb  35892  prv1n  35904  elmpps  36046  nmulprop  36663  nmulcom  36667  nmuladdel  36670  nmulrid  36678  cbvriotavw2  36729  cbvmpovw2  36735  cbvmpo1vw2  36736  cbvmpo2vw2  36737  cbvixpvw2  36738  cbvitgvw2  36741  cbvsbcdavw2  36751  cbvixpdavw  36771  cbvrmodavw2  36776  cbvreudavw2  36777  cbvmpodavw2  36784  cbvmpo1davw2  36785  cbvmpo2davw2  36786  cbvixpdavw2  36787  cbvproddavw2  36789  cbvitgdavw2  36790  weiunpo  36957  weiunso  36958  weiunfr  36959  weiunse  36960  bj-elabd2ALT  37542  bj-ru1  37560  currysetlem  37562  currysetlem1  37564  bj-ismoore  37728  csbfinxpg  38015  pibt2  38044  lindsadd  38245  lindsenlbs  38247  ptrest  38251  upixp  38361  sdclem1  38375  sstotbnd2  38406  prdsbnd2  38427  isprrngo  38682  isopos  39935  isatl  40054  aks6d1c1p6  42862  isnacs3  43424  nacsfix  43426  mzpclall  43441  dnnumch1  43754  dnwech  43758  aomclem3  43766  aomclem8  43771  dfac11  43772  islmodfg  43779  oaordnr  44006  omnord1  44015  oenord1  44026  cantnfresb  44034  rfovcnvf1od  44713  ismnu  44954  sblpnf  45003  rusbcALT  45131  cbvrabv2w  45829  choicefi  45900  climsuselem1  46306  climsuse  46307  cncfuni  46583  dvnprodlem1  46643  stoweidlem31  46728  stoweidlem59  46756  fourierdlem46  46849  fourierdlem62  46865  fourierdlem72  46875  fourierdlem79  46882  fourierdlem88  46891  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem112  46915  qndenserrnbllem  46991  ioorrnopnlem  47001  ioorrnopn  47002  ioorrnopnxr  47004  issal  47011  subsaliuncllem  47054  subsaliuncl  47055  subsalsal  47056  sge0tsms  47077  sge0iunmpt  47115  sge0seq  47143  ovnsubaddlem1  47267  ovnsubaddlem2  47268  hoidmvlelem3  47294  hoidmvlelem4  47295  rrnmbl  47311  hoiqssbllem3  47321  hspmbl  47326  hoimbl  47328  issmflem  47424  issmfd  47432  issmfdf  47434  smfpimltmpt  47443  issmfled  47454  smfpimltxrmptf  47455  smfmbfcex  47457  issmfgtd  47458  smflimlem1  47468  smflimlem2  47469  smflimlem3  47470  smflimlem6  47473  smfpimgtmpt  47478  smfpimgtxrmptf  47481  smfres  47487  smfpimcclem  47504  smfpimcc  47505  dfateq12d  47846  iscllaw  48937  isprmrng  49084  islininds  49209  brab2ddw  49590  brab2ddw2  49591  funcf2lem  49842  isthincd2lem2  50196  setc1onsubc  50363