Theorem eleq12d 2823

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  neleq12d  3035  cbvraldva2  3323  cbvrexdva2OLD  3325  cdeqel  3750  ruOLD  3755  sbceqbid  3763  cbvrabcsfw  3906  cbvralcsf  3907  cbvreucsf  3909  cbvrabcsf  3910  sbcel12  4377  elvvuni  5718  elrnmpt1  5927  canth  7344  onnseq  8316  smoeq  8322  smores  8324  smores2  8326  iordsmo  8329  tz7.49  8416  nnaordr  8587  omsmolem  8624  naddel2  8655  fvixp  8878  cbvixp  8890  cbvixpv  8891  mptelixpg  8911  boxcutc  8917  ixpiunwdom  9550  elirr  9557  cantnflt  9632  oemapvali  9644  cantnflem1  9649  cantnf  9653  wemapwe  9657  cnfcom3lem  9663  ttrcltr  9676  rnttrcl  9682  infxpen  9974  dfac8alem  9989  dfac8clem  9992  ac5num  9996  acni2  10006  numacn  10009  acndom  10011  aceq3lem  10080  dfac5  10089  dfac9  10097  dfac13  10103  fin2i  10255  isfin2-2  10279  fin23lem27  10288  isfin3ds  10289  fin23lem17  10298  fin23lem39  10310  isf33lem  10326  isf34lem7  10339  isf34lem6  10340  fin1a2lem10  10369  fin1a2lem12  10371  hsmexlem4  10389  axcc2lem  10396  axcc3  10398  domtriomlem  10402  axdc2lem  10408  axdc3lem2  10411  axdc3lem3  10412  axdc3lem4  10413  axdc3  10414  axdc4lem  10415  axcclem  10417  ac6num  10439  ac6c4  10441  iundom2g  10500  fpwwe2  10603  pwfseqlem1  10618  pwfseqlem4a  10621  pwfseqlem4  10622  ltapi  10863  ltmpi  10864  eluzaddOLD  12835  fzsubel  13528  elfzp1b  13569  axdc4uzlem  13955  wrd2ind  14695  smuval  16458  prdsbasprj  17442  xpsfrnel  17532  ismri2dad  17605  mreexd  17610  mreacs  17626  iscat  17640  iscatd  17641  iscatd2  17649  catcocl  17653  catpropd  17677  brssc  17783  issubc  17804  subcidcl  17813  subccocl  17814  isfunc  17833  isfuncd  17834  cofucl  17857  funcres2b  17866  fuciso  17947  yonedalem3  18248  yonffthlem  18250  ismgm  18575  ismgmd  18586  issstrmgm  18587  issgrpd  18664  ismndd  18690  eqgfval  19115  efgsdm  19667  efgsdmi  19669  efgsrel  19671  efgsp1  19674  efgsres  19675  dprdfcl  19952  ablfaclem3  20026  isdrngd  20681  isdrngdOLD  20683  issrng  20760  issrngd  20771  islmodd  20779  islbs  20990  lbsind  20994  lbspropd  21013  islbs2  21071  lbsextlem4  21078  lbsextg  21079  pzriprnglem8  21405  zndvds  21466  isphl  21544  isphld  21570  phlpropd  21571  frlmlbs  21713  islindf  21728  islinds2  21729  lindfind  21732  lindsind  21733  lindsind2  21735  lindfrn  21737  lindfmm  21743  lsslindf  21746  mhppwdeg  22044  mat1dimmul  22370  istps  22828  tpspropd  22832  eltpsg  22837  islp  23034  1stcelcls  23355  kgeni  23431  kgencn2  23451  ptpjpre1  23465  elptr2  23468  ptbasin  23471  ptbasfi  23475  ptpjcn  23505  ptpjopn  23506  ptcld  23507  ptcldmpt  23508  ptclsg  23509  ptcnp  23516  qtopval  23589  ptcmplem2  23947  ptcmplem3  23948  ptcmplem4  23949  istmd  23968  istgp  23971  tmdgsum  23989  istlm  24079  isusp  24156  prdsdsf  24262  prdsxmet  24264  isms  24344  mspropd  24369  setsxms  24374  setsms  24375  tmsxms  24381  tmsms  24382  isnrg  24555  tngnrg  24569  bcthlem2  25232  bcthlem3  25233  bcthlem4  25234  bcthlem5  25235  iscms  25252  cmspropd  25256  cmssmscld  25257  cmsss  25258  shft2rab  25416  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2lem5  25429  vitalilem2  25517  vitalilem3  25518  vitali  25521  limcfval  25780  limcmpt2  25792  limcres  25794  cnplimc  25795  cnlimci  25797  elcpn  25843  uc1pval  26052  ig1pcl  26091  jensen  26906  axtgcont  28403  tglngval  28485  ishlg  28536  mirbtwnb  28606  trgcopy  28738  trgcopyeu  28740  acopyeu  28768  isinagd  28773  tgasa1  28792  wlkp1lem3  29610  umgrwwlks2on  29894  clwwlknon1  30033  clwwlknonclwlknonf1o  30298  imsmet  30627  smcn  30634  iscbn  30800  sbceqbidf  32423  fnpreimac  32602  isslmd  33162  0nellinds  33348  lindssn  33356  lindfpropd  33360  elrspunidl  33406  lbslsat  33619  lindsunlem  33627  brfldext  33648  submateq  33806  lmatcl  33813  ispcmp  33854  zarcmplem  33878  zhmnrg  33962  ismntoplly  34022  sigapildsys  34159  fiunelcarsg  34314  eulerpartlemgvv  34374  eulerpart  34380  onvf1odlem2  35098  ptpconn  35227  cvmscbv  35252  cvmshmeo  35265  cvmsss2  35268  cvmliftlem7  35285  cvmliftlem10  35288  cvmlift2lem11  35307  cvmlift2lem12  35308  satffunlem1lem1  35396  satffunlem2lem1  35398  sategoelfvb  35413  prv1n  35425  elmpps  35567  cbvriotavw2  36231  cbvmpovw2  36237  cbvmpo1vw2  36238  cbvmpo2vw2  36239  cbvixpvw2  36240  cbvitgvw2  36243  cbvsbcdavw2  36253  cbvixpdavw  36273  cbvrmodavw2  36278  cbvreudavw2  36279  cbvmpodavw2  36286  cbvmpo1davw2  36287  cbvmpo2davw2  36288  cbvixpdavw2  36289  cbvproddavw2  36291  cbvitgdavw2  36292  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  bj-elabd2ALT  36920  bj-ru1  36938  currysetlem  36940  currysetlem1  36942  bj-ismoore  37100  csbfinxpg  37383  pibt2  37412  lindsadd  37614  lindsenlbs  37616  ptrest  37620  upixp  37730  sdclem1  37744  sstotbnd2  37775  prdsbnd2  37796  isprrngo  38051  isopos  39180  isatl  39299  aks6d1c1p6  42109  isnacs3  42705  nacsfix  42707  mzpclall  42722  dnnumch1  43040  dnwech  43044  aomclem3  43052  aomclem8  43057  dfac11  43058  islmodfg  43065  oaordnr  43292  omnord1  43301  oenord1  43312  cantnfresb  43320  rfovcnvf1od  44000  ismnu  44257  sblpnf  44306  rusbcALT  44435  cbvrabv2w  45129  choicefi  45201  climsuselem1  45612  climsuse  45613  cncfuni  45891  dvnprodlem1  45951  stoweidlem31  46036  stoweidlem59  46064  fourierdlem46  46157  fourierdlem62  46173  fourierdlem72  46183  fourierdlem79  46190  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem112  46223  qndenserrnbllem  46299  ioorrnopnlem  46309  ioorrnopn  46310  ioorrnopnxr  46312  issal  46319  subsaliuncllem  46362  subsaliuncl  46363  subsalsal  46364  sge0tsms  46385  sge0iunmpt  46423  sge0seq  46451  ovnsubaddlem1  46575  ovnsubaddlem2  46576  hoidmvlelem3  46602  hoidmvlelem4  46603  rrnmbl  46619  hoiqssbllem3  46629  hspmbl  46634  hoimbl  46636  issmflem  46732  issmfd  46740  issmfdf  46742  smfpimltmpt  46751  issmfled  46762  smfpimltxrmptf  46763  smfmbfcex  46765  issmfgtd  46766  smflimlem1  46776  smflimlem2  46777  smflimlem3  46778  smflimlem6  46781  smfpimgtmpt  46786  smfpimgtxrmptf  46789  smfres  46795  smfpimcclem  46812  smfpimcc  46813  dfateq12d  47131  iscllaw  48181  islininds  48439  brab2ddw  48821  brab2ddw2  48822  funcf2lem  49074  isthincd2lem2  49428  setc1onsubc  49595