Theorem eleq12d 2835

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

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

This theorem is referenced by:  neleq12d  3051  cbvraldva2  3348  cbvrexdva2OLD  3350  cdeqel  3782  ruOLD  3787  sbceqbid  3795  cbvrabcsfw  3940  cbvralcsf  3941  cbvreucsf  3943  cbvrabcsf  3944  sbcel12  4411  elvvuni  5762  elrnmpt1  5971  canth  7385  onnseq  8384  smoeq  8390  smores  8392  smores2  8394  iordsmo  8397  tz7.49  8485  nnaordr  8658  omsmolem  8695  naddel2  8726  fvixp  8942  cbvixp  8954  cbvixpv  8955  mptelixpg  8975  boxcutc  8981  ixpiunwdom  9630  elirr  9637  cantnflt  9712  oemapvali  9724  cantnflem1  9729  cantnf  9733  wemapwe  9737  cnfcom3lem  9743  ttrcltr  9756  rnttrcl  9762  infxpen  10054  dfac8alem  10069  dfac8clem  10072  ac5num  10076  acni2  10086  numacn  10089  acndom  10091  aceq3lem  10160  dfac5  10169  dfac9  10177  dfac13  10183  fin2i  10335  isfin2-2  10359  fin23lem27  10368  isfin3ds  10369  fin23lem17  10378  fin23lem39  10390  isf33lem  10406  isf34lem7  10419  isf34lem6  10420  fin1a2lem10  10449  fin1a2lem12  10451  hsmexlem4  10469  axcc2lem  10476  axcc3  10478  domtriomlem  10482  axdc2lem  10488  axdc3lem2  10491  axdc3lem3  10492  axdc3lem4  10493  axdc3  10494  axdc4lem  10495  axcclem  10497  ac6num  10519  ac6c4  10521  iundom2g  10580  fpwwe2  10683  pwfseqlem1  10698  pwfseqlem4a  10701  pwfseqlem4  10702  ltapi  10943  ltmpi  10944  eluzaddOLD  12913  fzsubel  13600  elfzp1b  13641  axdc4uzlem  14024  wrd2ind  14761  smuval  16518  prdsbasprj  17517  xpsfrnel  17607  ismri2dad  17680  mreexd  17685  mreacs  17701  iscat  17715  iscatd  17716  iscatd2  17724  catcocl  17728  catpropd  17752  brssc  17858  issubc  17880  subcidcl  17889  subccocl  17890  isfunc  17909  isfuncd  17910  cofucl  17933  funcres2b  17942  fuciso  18023  yonedalem3  18325  yonffthlem  18327  ismgm  18654  ismgmd  18665  issstrmgm  18666  issgrpd  18743  ismndd  18769  eqgfval  19194  efgsdm  19748  efgsdmi  19750  efgsrel  19752  efgsp1  19755  efgsres  19756  dprdfcl  20033  ablfaclem3  20107  isdrngd  20765  isdrngdOLD  20767  issrng  20845  issrngd  20856  islmodd  20864  islbs  21075  lbsind  21079  lbspropd  21098  islbs2  21156  lbsextlem4  21163  lbsextg  21164  pzriprnglem8  21499  zndvds  21568  isphl  21646  isphld  21672  phlpropd  21673  frlmlbs  21817  islindf  21832  islinds2  21833  lindfind  21836  lindsind  21837  lindsind2  21839  lindfrn  21841  lindfmm  21847  lsslindf  21850  mhppwdeg  22154  mat1dimmul  22482  istps  22940  tpspropd  22944  eltpsg  22949  eltpsgOLD  22950  islp  23148  1stcelcls  23469  kgeni  23545  kgencn2  23565  ptpjpre1  23579  elptr2  23582  ptbasin  23585  ptbasfi  23589  ptpjcn  23619  ptpjopn  23620  ptcld  23621  ptcldmpt  23622  ptclsg  23623  ptcnp  23630  qtopval  23703  ptcmplem2  24061  ptcmplem3  24062  ptcmplem4  24063  istmd  24082  istgp  24085  tmdgsum  24103  istlm  24193  isusp  24270  prdsdsf  24377  prdsxmet  24379  isms  24459  mspropd  24484  setsxms  24491  setsms  24492  tmsxms  24499  tmsms  24500  isnrg  24681  tngnrg  24695  bcthlem2  25359  bcthlem3  25360  bcthlem4  25361  bcthlem5  25362  iscms  25379  cmspropd  25383  cmssmscld  25384  cmsss  25385  shft2rab  25543  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2lem5  25556  vitalilem2  25644  vitalilem3  25645  vitali  25648  limcfval  25907  limcmpt2  25919  limcres  25921  cnplimc  25922  cnlimci  25924  elcpn  25970  uc1pval  26179  ig1pcl  26218  jensen  27032  axtgcont  28477  tglngval  28559  ishlg  28610  mirbtwnb  28680  trgcopy  28812  trgcopyeu  28814  acopyeu  28842  isinagd  28847  tgasa1  28866  wlkp1lem3  29693  umgrwwlks2on  29977  clwwlknon1  30116  clwwlknonclwlknonf1o  30381  imsmet  30710  smcn  30717  iscbn  30883  sbceqbidf  32506  fnpreimac  32681  isslmd  33208  0nellinds  33398  lindssn  33406  lindfpropd  33410  elrspunidl  33456  lbslsat  33667  lindsunlem  33675  brfldext  33698  submateq  33808  lmatcl  33815  ispcmp  33856  zarcmplem  33880  zhmnrg  33966  ismntoplly  34026  sigapildsys  34163  fiunelcarsg  34318  eulerpartlemgvv  34378  eulerpart  34384  ptpconn  35238  cvmscbv  35263  cvmshmeo  35276  cvmsss2  35279  cvmliftlem7  35296  cvmliftlem10  35299  cvmlift2lem11  35318  cvmlift2lem12  35319  satffunlem1lem1  35407  satffunlem2lem1  35409  sategoelfvb  35424  prv1n  35436  elmpps  35578  cbvriotavw2  36237  cbvmpovw2  36243  cbvmpo1vw2  36244  cbvmpo2vw2  36245  cbvixpvw2  36246  cbvitgvw2  36249  cbvsbcdavw2  36259  cbvixpdavw  36279  cbvrmodavw2  36284  cbvreudavw2  36285  cbvmpodavw2  36292  cbvmpo1davw2  36293  cbvmpo2davw2  36294  cbvixpdavw2  36295  cbvproddavw2  36297  cbvitgdavw2  36298  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  bj-elabd2ALT  36926  bj-ru1  36944  currysetlem  36946  currysetlem1  36948  bj-ismoore  37106  csbfinxpg  37389  pibt2  37418  lindsadd  37620  lindsenlbs  37622  ptrest  37626  upixp  37736  sdclem1  37750  sstotbnd2  37781  prdsbnd2  37802  isprrngo  38057  isopos  39181  isatl  39300  aks6d1c1p6  42115  isnacs3  42721  nacsfix  42723  mzpclall  42738  dnnumch1  43056  dnwech  43060  aomclem3  43068  aomclem8  43073  dfac11  43074  islmodfg  43081  oaordnr  43309  omnord1  43318  oenord1  43329  cantnfresb  43337  rfovcnvf1od  44017  ismnu  44280  sblpnf  44329  rusbcALT  44458  cbvrabv2w  45133  choicefi  45205  climsuselem1  45622  climsuse  45623  cncfuni  45901  dvnprodlem1  45961  stoweidlem31  46046  stoweidlem59  46074  fourierdlem46  46167  fourierdlem62  46183  fourierdlem72  46193  fourierdlem79  46200  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem112  46233  qndenserrnbllem  46309  ioorrnopnlem  46319  ioorrnopn  46320  ioorrnopnxr  46322  issal  46329  subsaliuncllem  46372  subsaliuncl  46373  subsalsal  46374  sge0tsms  46395  sge0iunmpt  46433  sge0seq  46461  ovnsubaddlem1  46585  ovnsubaddlem2  46586  hoidmvlelem3  46612  hoidmvlelem4  46613  rrnmbl  46629  hoiqssbllem3  46639  hspmbl  46644  hoimbl  46646  issmflem  46742  issmfd  46750  issmfdf  46752  smfpimltmpt  46761  issmfled  46772  smfpimltxrmptf  46773  smfmbfcex  46775  issmfgtd  46776  smflimlem1  46786  smflimlem2  46787  smflimlem3  46788  smflimlem6  46791  smfpimgtmpt  46796  smfpimgtxrmptf  46799  smfres  46805  smfpimcclem  46822  smfpimcc  46823  dfateq12d  47138  iscllaw  48105  islininds  48363  brab2ddw  48742  brab2ddw2  48743  funcf2lem  48914  isthincd2lem2  49084