Theorem eleq12d 2828

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  neleq12d  3041  cbvraldva2  3327  cbvrexdva2OLD  3329  cdeqel  3759  ruOLD  3764  sbceqbid  3772  cbvrabcsfw  3915  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  sbcel12  4386  elvvuni  5731  elrnmpt1  5940  canth  7357  onnseq  8356  smoeq  8362  smores  8364  smores2  8366  iordsmo  8369  tz7.49  8457  nnaordr  8630  omsmolem  8667  naddel2  8698  fvixp  8914  cbvixp  8926  cbvixpv  8927  mptelixpg  8947  boxcutc  8953  ixpiunwdom  9602  elirr  9609  cantnflt  9684  oemapvali  9696  cantnflem1  9701  cantnf  9705  wemapwe  9709  cnfcom3lem  9715  ttrcltr  9728  rnttrcl  9734  infxpen  10026  dfac8alem  10041  dfac8clem  10044  ac5num  10048  acni2  10058  numacn  10061  acndom  10063  aceq3lem  10132  dfac5  10141  dfac9  10149  dfac13  10155  fin2i  10307  isfin2-2  10331  fin23lem27  10340  isfin3ds  10341  fin23lem17  10350  fin23lem39  10362  isf33lem  10378  isf34lem7  10391  isf34lem6  10392  fin1a2lem10  10421  fin1a2lem12  10423  hsmexlem4  10441  axcc2lem  10448  axcc3  10450  domtriomlem  10454  axdc2lem  10460  axdc3lem2  10463  axdc3lem3  10464  axdc3lem4  10465  axdc3  10466  axdc4lem  10467  axcclem  10469  ac6num  10491  ac6c4  10493  iundom2g  10552  fpwwe2  10655  pwfseqlem1  10670  pwfseqlem4a  10673  pwfseqlem4  10674  ltapi  10915  ltmpi  10916  eluzaddOLD  12885  fzsubel  13575  elfzp1b  13616  axdc4uzlem  13999  wrd2ind  14739  smuval  16498  prdsbasprj  17484  xpsfrnel  17574  ismri2dad  17647  mreexd  17652  mreacs  17668  iscat  17682  iscatd  17683  iscatd2  17691  catcocl  17695  catpropd  17719  brssc  17825  issubc  17846  subcidcl  17855  subccocl  17856  isfunc  17875  isfuncd  17876  cofucl  17899  funcres2b  17908  fuciso  17989  yonedalem3  18290  yonffthlem  18292  ismgm  18617  ismgmd  18628  issstrmgm  18629  issgrpd  18706  ismndd  18732  eqgfval  19157  efgsdm  19709  efgsdmi  19711  efgsrel  19713  efgsp1  19716  efgsres  19717  dprdfcl  19994  ablfaclem3  20068  isdrngd  20723  isdrngdOLD  20725  issrng  20802  issrngd  20813  islmodd  20821  islbs  21032  lbsind  21036  lbspropd  21055  islbs2  21113  lbsextlem4  21120  lbsextg  21121  pzriprnglem8  21447  zndvds  21508  isphl  21586  isphld  21612  phlpropd  21613  frlmlbs  21755  islindf  21770  islinds2  21771  lindfind  21774  lindsind  21775  lindsind2  21777  lindfrn  21779  lindfmm  21785  lsslindf  21788  mhppwdeg  22086  mat1dimmul  22412  istps  22870  tpspropd  22874  eltpsg  22879  islp  23076  1stcelcls  23397  kgeni  23473  kgencn2  23493  ptpjpre1  23507  elptr2  23510  ptbasin  23513  ptbasfi  23517  ptpjcn  23547  ptpjopn  23548  ptcld  23549  ptcldmpt  23550  ptclsg  23551  ptcnp  23558  qtopval  23631  ptcmplem2  23989  ptcmplem3  23990  ptcmplem4  23991  istmd  24010  istgp  24013  tmdgsum  24031  istlm  24121  isusp  24198  prdsdsf  24304  prdsxmet  24306  isms  24386  mspropd  24411  setsxms  24416  setsms  24417  tmsxms  24423  tmsms  24424  isnrg  24597  tngnrg  24611  bcthlem2  25275  bcthlem3  25276  bcthlem4  25277  bcthlem5  25278  iscms  25295  cmspropd  25299  cmssmscld  25300  cmsss  25301  shft2rab  25459  ovolicc2lem3  25470  ovolicc2lem4  25471  ovolicc2lem5  25472  vitalilem2  25560  vitalilem3  25561  vitali  25564  limcfval  25823  limcmpt2  25835  limcres  25837  cnplimc  25838  cnlimci  25840  elcpn  25886  uc1pval  26095  ig1pcl  26134  jensen  26949  axtgcont  28394  tglngval  28476  ishlg  28527  mirbtwnb  28597  trgcopy  28729  trgcopyeu  28731  acopyeu  28759  isinagd  28764  tgasa1  28783  wlkp1lem3  29601  umgrwwlks2on  29885  clwwlknon1  30024  clwwlknonclwlknonf1o  30289  imsmet  30618  smcn  30625  iscbn  30791  sbceqbidf  32414  fnpreimac  32595  isslmd  33145  0nellinds  33331  lindssn  33339  lindfpropd  33343  elrspunidl  33389  lbslsat  33602  lindsunlem  33610  brfldext  33633  submateq  33786  lmatcl  33793  ispcmp  33834  zarcmplem  33858  zhmnrg  33942  ismntoplly  34002  sigapildsys  34139  fiunelcarsg  34294  eulerpartlemgvv  34354  eulerpart  34360  ptpconn  35201  cvmscbv  35226  cvmshmeo  35239  cvmsss2  35242  cvmliftlem7  35259  cvmliftlem10  35262  cvmlift2lem11  35281  cvmlift2lem12  35282  satffunlem1lem1  35370  satffunlem2lem1  35372  sategoelfvb  35387  prv1n  35399  elmpps  35541  cbvriotavw2  36200  cbvmpovw2  36206  cbvmpo1vw2  36207  cbvmpo2vw2  36208  cbvixpvw2  36209  cbvitgvw2  36212  cbvsbcdavw2  36222  cbvixpdavw  36242  cbvrmodavw2  36247  cbvreudavw2  36248  cbvmpodavw2  36255  cbvmpo1davw2  36256  cbvmpo2davw2  36257  cbvixpdavw2  36258  cbvproddavw2  36260  cbvitgdavw2  36261  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  bj-elabd2ALT  36889  bj-ru1  36907  currysetlem  36909  currysetlem1  36911  bj-ismoore  37069  csbfinxpg  37352  pibt2  37381  lindsadd  37583  lindsenlbs  37585  ptrest  37589  upixp  37699  sdclem1  37713  sstotbnd2  37744  prdsbnd2  37765  isprrngo  38020  isopos  39144  isatl  39263  aks6d1c1p6  42073  isnacs3  42680  nacsfix  42682  mzpclall  42697  dnnumch1  43015  dnwech  43019  aomclem3  43027  aomclem8  43032  dfac11  43033  islmodfg  43040  oaordnr  43267  omnord1  43276  oenord1  43287  cantnfresb  43295  rfovcnvf1od  43975  ismnu  44233  sblpnf  44282  rusbcALT  44411  cbvrabv2w  45100  choicefi  45172  climsuselem1  45584  climsuse  45585  cncfuni  45863  dvnprodlem1  45923  stoweidlem31  46008  stoweidlem59  46036  fourierdlem46  46129  fourierdlem62  46145  fourierdlem72  46155  fourierdlem79  46162  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem112  46195  qndenserrnbllem  46271  ioorrnopnlem  46281  ioorrnopn  46282  ioorrnopnxr  46284  issal  46291  subsaliuncllem  46334  subsaliuncl  46335  subsalsal  46336  sge0tsms  46357  sge0iunmpt  46395  sge0seq  46423  ovnsubaddlem1  46547  ovnsubaddlem2  46548  hoidmvlelem3  46574  hoidmvlelem4  46575  rrnmbl  46591  hoiqssbllem3  46601  hspmbl  46606  hoimbl  46608  issmflem  46704  issmfd  46712  issmfdf  46714  smfpimltmpt  46723  issmfled  46734  smfpimltxrmptf  46735  smfmbfcex  46737  issmfgtd  46738  smflimlem1  46748  smflimlem2  46749  smflimlem3  46750  smflimlem6  46753  smfpimgtmpt  46758  smfpimgtxrmptf  46761  smfres  46767  smfpimcclem  46784  smfpimcc  46785  dfateq12d  47103  iscllaw  48112  islininds  48370  brab2ddw  48755  brab2ddw2  48756  funcf2lem  48994  isthincd2lem2  49269  setc1onsubc  49427