Theorem eleq12d 2834

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815

This theorem is referenced by:  neleq12d  3044  cbvraldva2  3316  cdeqel  3724  ruOLD  3729  sbceqbid  3737  cbvrabcsfw  3879  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  sbcel12  4346  elvvuni  5702  elrnmpt1  5909  canth  7317  onnseq  8281  smoeq  8287  smores  8289  smores2  8291  iordsmo  8294  tz7.49  8381  nnaordr  8553  omsmolem  8590  naddel2  8621  fvixp  8847  cbvixp  8859  cbvixpv  8860  mptelixpg  8880  boxcutc  8886  ixpiunwdom  9502  elirr  9512  cantnflt  9591  oemapvali  9603  cantnflem1  9608  cantnf  9612  wemapwe  9616  cnfcom3lem  9622  ttrcltr  9635  rnttrcl  9641  infxpen  9934  dfac8alem  9949  dfac8clem  9952  ac5num  9956  acni2  9966  numacn  9969  acndom  9971  aceq3lem  10040  dfac5  10049  dfac9  10057  dfac13  10063  fin2i  10215  isfin2-2  10239  fin23lem27  10248  isfin3ds  10249  fin23lem17  10258  fin23lem39  10270  isf33lem  10286  isf34lem7  10299  isf34lem6  10300  fin1a2lem10  10329  fin1a2lem12  10331  hsmexlem4  10349  axcc2lem  10356  axcc3  10358  domtriomlem  10362  axdc2lem  10368  axdc3lem2  10371  axdc3lem3  10372  axdc3lem4  10373  axdc3  10374  axdc4lem  10375  axcclem  10377  ac6num  10399  ac6c4  10401  iundom2g  10460  fpwwe2  10564  pwfseqlem1  10579  pwfseqlem4a  10582  pwfseqlem4  10583  ltapi  10824  ltmpi  10825  fzsubel  13512  elfzp1b  13553  axdc4uzlem  13943  wrd2ind  14683  smuval  16448  prdsbasprj  17433  xpsfrnel  17524  ismri2dad  17601  mreexd  17606  mreacs  17622  iscat  17636  iscatd  17637  iscatd2  17645  catcocl  17649  catpropd  17673  brssc  17779  issubc  17800  subcidcl  17809  subccocl  17810  isfunc  17829  isfuncd  17830  cofucl  17853  funcres2b  17862  fuciso  17943  yonedalem3  18244  yonffthlem  18246  ismgm  18607  ismgmd  18618  issstrmgm  18619  issgrpd  18696  ismndd  18722  eqgfval  19149  efgsdm  19703  efgsdmi  19705  efgsrel  19707  efgsp1  19710  efgsres  19711  dprdfcl  19988  ablfaclem3  20062  isdrngd  20744  isdrngdOLD  20746  issrng  20823  issrngd  20834  islmodd  20863  islbs  21073  lbsind  21077  lbspropd  21096  islbs2  21154  lbsextlem4  21161  lbsextg  21162  pzriprnglem8  21470  zndvds  21531  isphl  21610  isphld  21636  phlpropd  21637  frlmlbs  21779  islindf  21794  islinds2  21795  lindfind  21798  lindsind  21799  lindsind2  21801  lindfrn  21803  lindfmm  21809  lsslindf  21812  mhppwdeg  22145  mat1dimmul  22466  istps  22924  tpspropd  22928  eltpsg  22933  islp  23130  1stcelcls  23451  kgeni  23527  kgencn2  23547  ptpjpre1  23561  elptr2  23564  ptbasin  23567  ptbasfi  23571  ptpjcn  23601  ptpjopn  23602  ptcld  23603  ptcldmpt  23604  ptclsg  23605  ptcnp  23612  qtopval  23685  ptcmplem2  24043  ptcmplem3  24044  ptcmplem4  24045  istmd  24064  istgp  24067  tmdgsum  24085  istlm  24175  isusp  24251  prdsdsf  24357  prdsxmet  24359  isms  24439  mspropd  24464  setsxms  24469  setsms  24470  tmsxms  24476  tmsms  24477  isnrg  24650  tngnrg  24664  bcthlem2  25317  bcthlem3  25318  bcthlem4  25319  bcthlem5  25320  iscms  25337  cmspropd  25341  cmssmscld  25342  cmsss  25343  shft2rab  25500  ovolicc2lem3  25511  ovolicc2lem4  25512  ovolicc2lem5  25513  vitalilem2  25601  vitalilem3  25602  vitali  25605  limcfval  25864  limcmpt2  25876  limcres  25878  cnplimc  25879  cnlimci  25881  elcpn  25926  uc1pval  26130  ig1pcl  26169  jensen  26977  axtgcont  28562  tglngval  28644  ishlg  28695  mirbtwnb  28765  trgcopy  28897  trgcopyeu  28899  acopyeu  28927  isinagd  28932  tgasa1  28951  wlkp1lem3  29767  usgrwwlks2on  30051  umgrwwlks2on  30052  clwwlknon1  30192  clwwlknonclwlknonf1o  30457  imsmet  30787  smcn  30794  iscbn  30960  sbceqbidf  32581  fnpreimac  32769  isslmd  33290  0nellinds  33460  lindssn  33468  lindfpropd  33472  elrspunidl  33518  lbslsat  33807  lindsunlem  33815  brfldext  33836  submateq  34000  lmatcl  34007  ispcmp  34048  zarcmplem  34072  zhmnrg  34156  ismntoplly  34216  sigapildsys  34353  fiunelcarsg  34507  eulerpartlemgvv  34567  eulerpart  34573  fineqvinfep  35313  onvf1odlem2  35339  ptpconn  35468  cvmscbv  35493  cvmshmeo  35506  cvmsss2  35509  cvmliftlem7  35526  cvmliftlem10  35529  cvmlift2lem11  35548  cvmlift2lem12  35549  satffunlem1lem1  35637  satffunlem2lem1  35639  sategoelfvb  35654  prv1n  35666  elmpps  35808  cbvriotavw2  36471  cbvmpovw2  36477  cbvmpo1vw2  36478  cbvmpo2vw2  36479  cbvixpvw2  36480  cbvitgvw2  36483  cbvsbcdavw2  36493  cbvixpdavw  36513  cbvrmodavw2  36518  cbvreudavw2  36519  cbvmpodavw2  36526  cbvmpo1davw2  36527  cbvmpo2davw2  36528  cbvixpdavw2  36529  cbvproddavw2  36531  cbvitgdavw2  36532  weiunpo  36700  weiunso  36701  weiunfr  36702  weiunse  36703  bj-elabd2ALT  37285  bj-ru1  37303  currysetlem  37305  currysetlem1  37307  bj-ismoore  37470  csbfinxpg  37757  pibt2  37786  lindsadd  37987  lindsenlbs  37989  ptrest  37993  upixp  38103  sdclem1  38117  sstotbnd2  38148  prdsbnd2  38169  isprrngo  38424  isopos  39679  isatl  39798  aks6d1c1p6  42606  isnacs3  43166  nacsfix  43168  mzpclall  43183  dnnumch1  43496  dnwech  43500  aomclem3  43508  aomclem8  43513  dfac11  43514  islmodfg  43521  oaordnr  43748  omnord1  43757  oenord1  43768  cantnfresb  43776  rfovcnvf1od  44455  ismnu  44712  sblpnf  44761  rusbcALT  44889  cbvrabv2w  45582  choicefi  45653  climsuselem1  46059  climsuse  46060  cncfuni  46336  dvnprodlem1  46396  stoweidlem31  46481  stoweidlem59  46509  fourierdlem46  46602  fourierdlem62  46618  fourierdlem72  46628  fourierdlem79  46635  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem112  46668  qndenserrnbllem  46744  ioorrnopnlem  46754  ioorrnopn  46755  ioorrnopnxr  46757  issal  46764  subsaliuncllem  46807  subsaliuncl  46808  subsalsal  46809  sge0tsms  46830  sge0iunmpt  46868  sge0seq  46896  ovnsubaddlem1  47020  ovnsubaddlem2  47021  hoidmvlelem3  47047  hoidmvlelem4  47048  rrnmbl  47064  hoiqssbllem3  47074  hspmbl  47079  hoimbl  47081  issmflem  47177  issmfd  47185  issmfdf  47187  smfpimltmpt  47196  issmfled  47207  smfpimltxrmptf  47208  smfmbfcex  47210  issmfgtd  47211  smflimlem1  47221  smflimlem2  47222  smflimlem3  47223  smflimlem6  47226  smfpimgtmpt  47231  smfpimgtxrmptf  47234  smfres  47240  smfpimcclem  47257  smfpimcc  47258  dfateq12d  47596  iscllaw  48687  islininds  48944  brab2ddw  49326  brab2ddw2  49327  funcf2lem  49578  isthincd2lem2  49932  setc1onsubc  50099