Theorem eleq12d 2822

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

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

This theorem is referenced by:  neleq12d  3034  cbvraldva2  3321  cbvrexdva2OLD  3323  cdeqel  3747  ruOLD  3752  sbceqbid  3760  cbvrabcsfw  3903  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  sbcel12  4374  elvvuni  5715  elrnmpt1  5924  canth  7341  onnseq  8313  smoeq  8319  smores  8321  smores2  8323  iordsmo  8326  tz7.49  8413  nnaordr  8584  omsmolem  8621  naddel2  8652  fvixp  8875  cbvixp  8887  cbvixpv  8888  mptelixpg  8908  boxcutc  8914  ixpiunwdom  9543  elirr  9550  cantnflt  9625  oemapvali  9637  cantnflem1  9642  cantnf  9646  wemapwe  9650  cnfcom3lem  9656  ttrcltr  9669  rnttrcl  9675  infxpen  9967  dfac8alem  9982  dfac8clem  9985  ac5num  9989  acni2  9999  numacn  10002  acndom  10004  aceq3lem  10073  dfac5  10082  dfac9  10090  dfac13  10096  fin2i  10248  isfin2-2  10272  fin23lem27  10281  isfin3ds  10282  fin23lem17  10291  fin23lem39  10303  isf33lem  10319  isf34lem7  10332  isf34lem6  10333  fin1a2lem10  10362  fin1a2lem12  10364  hsmexlem4  10382  axcc2lem  10389  axcc3  10391  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  axdc3lem3  10405  axdc3lem4  10406  axdc3  10407  axdc4lem  10408  axcclem  10410  ac6num  10432  ac6c4  10434  iundom2g  10493  fpwwe2  10596  pwfseqlem1  10611  pwfseqlem4a  10614  pwfseqlem4  10615  ltapi  10856  ltmpi  10857  eluzaddOLD  12828  fzsubel  13521  elfzp1b  13562  axdc4uzlem  13948  wrd2ind  14688  smuval  16451  prdsbasprj  17435  xpsfrnel  17525  ismri2dad  17598  mreexd  17603  mreacs  17619  iscat  17633  iscatd  17634  iscatd2  17642  catcocl  17646  catpropd  17670  brssc  17776  issubc  17797  subcidcl  17806  subccocl  17807  isfunc  17826  isfuncd  17827  cofucl  17850  funcres2b  17859  fuciso  17940  yonedalem3  18241  yonffthlem  18243  ismgm  18568  ismgmd  18579  issstrmgm  18580  issgrpd  18657  ismndd  18683  eqgfval  19108  efgsdm  19660  efgsdmi  19662  efgsrel  19664  efgsp1  19667  efgsres  19668  dprdfcl  19945  ablfaclem3  20019  isdrngd  20674  isdrngdOLD  20676  issrng  20753  issrngd  20764  islmodd  20772  islbs  20983  lbsind  20987  lbspropd  21006  islbs2  21064  lbsextlem4  21071  lbsextg  21072  pzriprnglem8  21398  zndvds  21459  isphl  21537  isphld  21563  phlpropd  21564  frlmlbs  21706  islindf  21721  islinds2  21722  lindfind  21725  lindsind  21726  lindsind2  21728  lindfrn  21730  lindfmm  21736  lsslindf  21739  mhppwdeg  22037  mat1dimmul  22363  istps  22821  tpspropd  22825  eltpsg  22830  islp  23027  1stcelcls  23348  kgeni  23424  kgencn2  23444  ptpjpre1  23458  elptr2  23461  ptbasin  23464  ptbasfi  23468  ptpjcn  23498  ptpjopn  23499  ptcld  23500  ptcldmpt  23501  ptclsg  23502  ptcnp  23509  qtopval  23582  ptcmplem2  23940  ptcmplem3  23941  ptcmplem4  23942  istmd  23961  istgp  23964  tmdgsum  23982  istlm  24072  isusp  24149  prdsdsf  24255  prdsxmet  24257  isms  24337  mspropd  24362  setsxms  24367  setsms  24368  tmsxms  24374  tmsms  24375  isnrg  24548  tngnrg  24562  bcthlem2  25225  bcthlem3  25226  bcthlem4  25227  bcthlem5  25228  iscms  25245  cmspropd  25249  cmssmscld  25250  cmsss  25251  shft2rab  25409  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  vitalilem2  25510  vitalilem3  25511  vitali  25514  limcfval  25773  limcmpt2  25785  limcres  25787  cnplimc  25788  cnlimci  25790  elcpn  25836  uc1pval  26045  ig1pcl  26084  jensen  26899  axtgcont  28396  tglngval  28478  ishlg  28529  mirbtwnb  28599  trgcopy  28731  trgcopyeu  28733  acopyeu  28761  isinagd  28766  tgasa1  28785  wlkp1lem3  29603  umgrwwlks2on  29887  clwwlknon1  30026  clwwlknonclwlknonf1o  30291  imsmet  30620  smcn  30627  iscbn  30793  sbceqbidf  32416  fnpreimac  32595  isslmd  33155  0nellinds  33341  lindssn  33349  lindfpropd  33353  elrspunidl  33399  lbslsat  33612  lindsunlem  33620  brfldext  33641  submateq  33799  lmatcl  33806  ispcmp  33847  zarcmplem  33871  zhmnrg  33955  ismntoplly  34015  sigapildsys  34152  fiunelcarsg  34307  eulerpartlemgvv  34367  eulerpart  34373  onvf1odlem2  35091  ptpconn  35220  cvmscbv  35245  cvmshmeo  35258  cvmsss2  35261  cvmliftlem7  35278  cvmliftlem10  35281  cvmlift2lem11  35300  cvmlift2lem12  35301  satffunlem1lem1  35389  satffunlem2lem1  35391  sategoelfvb  35406  prv1n  35418  elmpps  35560  cbvriotavw2  36224  cbvmpovw2  36230  cbvmpo1vw2  36231  cbvmpo2vw2  36232  cbvixpvw2  36233  cbvitgvw2  36236  cbvsbcdavw2  36246  cbvixpdavw  36266  cbvrmodavw2  36271  cbvreudavw2  36272  cbvmpodavw2  36279  cbvmpo1davw2  36280  cbvmpo2davw2  36281  cbvixpdavw2  36282  cbvproddavw2  36284  cbvitgdavw2  36285  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  bj-elabd2ALT  36913  bj-ru1  36931  currysetlem  36933  currysetlem1  36935  bj-ismoore  37093  csbfinxpg  37376  pibt2  37405  lindsadd  37607  lindsenlbs  37609  ptrest  37613  upixp  37723  sdclem1  37737  sstotbnd2  37768  prdsbnd2  37789  isprrngo  38044  isopos  39173  isatl  39292  aks6d1c1p6  42102  isnacs3  42698  nacsfix  42700  mzpclall  42715  dnnumch1  43033  dnwech  43037  aomclem3  43045  aomclem8  43050  dfac11  43051  islmodfg  43058  oaordnr  43285  omnord1  43294  oenord1  43305  cantnfresb  43313  rfovcnvf1od  43993  ismnu  44250  sblpnf  44299  rusbcALT  44428  cbvrabv2w  45122  choicefi  45194  climsuselem1  45605  climsuse  45606  cncfuni  45884  dvnprodlem1  45944  stoweidlem31  46029  stoweidlem59  46057  fourierdlem46  46150  fourierdlem62  46166  fourierdlem72  46176  fourierdlem79  46183  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem112  46216  qndenserrnbllem  46292  ioorrnopnlem  46302  ioorrnopn  46303  ioorrnopnxr  46305  issal  46312  subsaliuncllem  46355  subsaliuncl  46356  subsalsal  46357  sge0tsms  46378  sge0iunmpt  46416  sge0seq  46444  ovnsubaddlem1  46568  ovnsubaddlem2  46569  hoidmvlelem3  46595  hoidmvlelem4  46596  rrnmbl  46612  hoiqssbllem3  46622  hspmbl  46627  hoimbl  46629  issmflem  46725  issmfd  46733  issmfdf  46735  smfpimltmpt  46744  issmfled  46755  smfpimltxrmptf  46756  smfmbfcex  46758  issmfgtd  46759  smflimlem1  46769  smflimlem2  46770  smflimlem3  46771  smflimlem6  46774  smfpimgtmpt  46779  smfpimgtxrmptf  46782  smfres  46788  smfpimcclem  46805  smfpimcc  46806  dfateq12d  47127  iscllaw  48177  islininds  48435  brab2ddw  48817  brab2ddw2  48818  funcf2lem  49070  isthincd2lem2  49424  setc1onsubc  49591