Theorem eleq12d 2877

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637   ∈ wcel 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2782

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2797  df-clel 2800

This theorem is referenced by:  neleq12d  3083  cbvraldva2  3362  cbvrexdva2  3363  cdeqel  3627  ru  3630  sbceqbid  3638  cbvralcsf  3758  cbvreucsf  3760  cbvrabcsf  3761  sbcel12  4178  elvvuni  5377  elrnmpt1  5573  canth  6830  onnseq  7675  smoeq  7681  smores  7683  smores2  7685  iordsmo  7688  tz7.49  7774  nnaordr  7935  omsmolem  7968  fvixp  8148  cbvixp  8160  mptelixpg  8180  boxcutc  8186  ixpiunwdom  8733  elirr  8739  cantnflt  8814  oemapvali  8826  cantnflem1  8831  cantnf  8835  wemapwe  8839  cnfcom3lem  8845  infxpen  9118  dfac8alem  9133  dfac8clem  9136  ac5num  9140  acni2  9150  numacn  9153  acndom  9155  aceq3lem  9224  dfac5  9232  dfac9  9241  dfac13  9247  fin2i  9400  isfin2-2  9424  fin23lem27  9433  isfin3ds  9434  fin23lem17  9443  fin23lem39  9455  isf33lem  9471  isf34lem7  9484  isf34lem6  9485  fin1a2lem10  9514  fin1a2lem12  9516  hsmexlem4  9534  axcc2lem  9541  axcc3  9543  domtriomlem  9547  axdc2lem  9553  axdc3lem2  9556  axdc3lem3  9557  axdc3lem4  9558  axdc3  9559  axdc4lem  9560  axcclem  9562  ac6num  9584  ac6c4  9586  iundom2g  9645  fpwwe2  9748  pwfseqlem1  9763  pwfseqlem4a  9766  pwfseqlem4  9767  ltapi  10008  ltmpi  10009  eluzadd  11931  fzsubel  12598  elfzp1b  12638  axdc4uzlem  13004  wrd2ind  13699  smuval  15420  prdsbasprj  16335  xpsfrnel  16426  ismri2dad  16500  mreexd  16505  mreacs  16521  iscat  16535  iscatd  16536  iscatd2  16544  catcocl  16548  catpropd  16571  brssc  16676  issubc  16697  subcidcl  16706  subccocl  16707  isfunc  16726  isfuncd  16727  cofucl  16750  funcres2b  16759  fuciso  16837  yonedalem3  17123  yonffthlem  17125  ismgm  17446  issstrmgm  17455  ismndd  17516  eqgfval  17842  efgsdm  18342  efgsdmi  18344  efgsrel  18346  efgsp1  18349  efgsres  18350  dprdfcl  18612  ablfaclem3  18686  isdrngd  18974  issrng  19052  issrngd  19063  islmodd  19071  islbs  19281  lbsind  19285  lbspropd  19304  islbs2  19361  lbsextlem4  19368  lbsextg  19369  zndvds  20103  isphl  20181  isphld  20207  phlpropd  20208  frlmlbs  20344  islindf  20359  islinds2  20360  lindfind  20363  lindsind  20364  lindsind2  20366  lindfrn  20368  lindfmm  20374  lsslindf  20377  mat1dimmul  20491  istps  20950  tpspropd  20954  eltpsg  20959  islp  21156  1stcelcls  21476  kgeni  21552  kgencn2  21572  ptpjpre1  21586  elptr2  21589  ptbasin  21592  ptbasfi  21596  ptpjcn  21626  ptpjopn  21627  ptcld  21628  ptcldmpt  21629  ptclsg  21630  ptcnp  21637  qtopval  21710  ptcmplem2  22068  ptcmplem3  22069  ptcmplem4  22070  istmd  22089  istgp  22092  tmdgsum  22110  istlm  22199  isusp  22276  prdsdsf  22383  prdsxmet  22385  isms  22465  mspropd  22490  setsxms  22495  setsms  22496  tmsxms  22502  tmsms  22503  isnrg  22675  tngnrg  22689  bcthlem2  23332  bcthlem3  23333  bcthlem4  23334  bcthlem5  23335  iscms  23352  cmspropd  23356  cmsss  23357  shft2rab  23487  ovolicc2lem3  23498  ovolicc2lem4  23499  ovolicc2lem5  23500  vitalilem2  23588  vitalilem3  23589  vitali  23592  limcfval  23848  limcmpt2  23860  limcres  23862  cnplimc  23863  cnlimci  23865  elcpn  23909  uc1pval  24111  ig1pcl  24147  jensen  24927  axtgcont  25580  tglngval  25658  ishlg  25709  mirbtwnb  25779  islnopp  25843  outpasch  25859  colhp  25874  trgcopy  25908  trgcopyeu  25910  dfcgra2  25933  acopyeu  25937  isinag  25941  tgasa1  25951  wlkp1lem3  26798  umgrwwlks2on  27096  clwwlknon1  27263  clwwlknonclwlknonf1o  27540  imsmet  27872  smcn  27879  iscbn  28046  sbceqbidf  29647  isslmd  30078  submateq  30198  lmatcl  30205  ispcmp  30247  zhmnrg  30334  ismntoplly  30392  inelpisys  30540  sigapildsys  30548  fiunelcarsg  30701  eulerpartlemgvv  30761  eulerpart  30767  ptpconn  31536  cvmscbv  31561  cvmshmeo  31574  cvmsss2  31577  cvmliftlem7  31594  cvmliftlem10  31597  cvmlift2lem11  31616  cvmlift2lem12  31617  elmpps  31791  bj-ismoore  33368  csbfinxpg  33539  lindsenlbs  33715  ptrest  33719  upixp  33834  sdclem1  33848  sstotbnd2  33882  prdsbnd2  33903  isprrngo  34158  isopos  34958  isatl  35077  isnacs3  37773  nacsfix  37775  mzpclall  37790  dnnumch1  38113  dnwech  38117  aomclem3  38125  aomclem8  38130  dfac11  38131  islmodfg  38138  rfovcnvf1od  38796  sblpnf  39007  rusbcALT  39137  sbcel12gOLD  39250  choicefi  39877  climsuselem1  40317  climsuse  40318  cncfuni  40577  dvnprodlem1  40639  stoweidlem31  40725  stoweidlem59  40753  fourierdlem46  40846  fourierdlem62  40862  fourierdlem72  40872  fourierdlem79  40879  fourierdlem88  40888  fourierdlem89  40889  fourierdlem90  40890  fourierdlem91  40891  fourierdlem112  40912  qndenserrnbllem  40991  ioorrnopnlem  41001  ioorrnopn  41002  ioorrnopnxr  41004  issal  41011  subsaliuncllem  41052  subsaliuncl  41053  subsalsal  41054  sge0tsms  41074  sge0iunmpt  41112  sge0seq  41140  ovnsubaddlem1  41264  ovnsubaddlem2  41265  hoidmvlelem3  41291  hoidmvlelem4  41292  rrnmbl  41308  hoiqssbllem3  41318  hspmbl  41323  hoimbl  41325  issmflem  41416  issmfd  41424  issmfdf  41426  smfpimltmpt  41435  issmfled  41446  smfpimltxrmpt  41447  smfmbfcex  41448  issmfgtd  41449  smflimlem1  41459  smflimlem2  41460  smflimlem3  41461  smflimlem6  41464  smfpimgtmpt  41469  smfpimgtxrmpt  41472  smfres  41477  smfco  41489  smfpimcclem  41493  smfpimcc  41494  dfateq12d  41713  ismgmd  42342  iscllaw  42391  islininds  42801