MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbequ12 Structured version   Visualization version   GIF version

Theorem sbequ12 2249
Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)
Assertion
Ref Expression
sbequ12 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2245 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 2246 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 214 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  [wsb 2065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-12 2173
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066
This theorem is referenced by:  sbequ12r  2250  sbequ12a  2252  sb5  2272  sb8v  2369  sb8ev  2370  sbbib  2376  axc16ALT  2524  nfsb4t  2535  sbco2  2549  sb8  2555  sb8e  2556  sbal1  2568  sbal2  2569  clelab  2958  sbab  2960  nfabdw  3000  cbvralfw  3437  cbvralf  3439  cbvralsvw  3467  cbvrexsvw  3468  cbvralsv  3469  cbvrexsv  3470  cbvrabw  3489  cbvrab  3490  sbhypf  3552  mob2  3705  reu2  3715  reu6  3716  sbcralt  3854  sbcreu  3858  cbvrabcsfw  3923  cbvreucsf  3926  cbvrabcsf  3927  csbif  4521  cbvopab1  5138  cbvopab1g  5139  cbvopab1s  5141  cbvmptf  5164  cbvmptfg  5165  opelopabsb  5416  csbopab  5441  csbopabgALT  5442  opeliunxp  5618  ralxpf  5716  cbviotaw  6320  cbviota  6322  csbiota  6347  f1ossf1o  6889  cbvriotaw  7122  cbvriota  7126  csbriota  7128  onminex  7521  tfis  7568  findes  7611  abrexex2g  7664  opabex3d  7665  opabex3rd  7666  opabex3  7667  dfoprab4f  7753  uzind4s  12307  ac6sf2  30369  esumcvg  31345  wl-sb8t  34787  wl-sbalnae  34797  wl-ax11-lem8  34823  sbcrexgOLD  39382  scottabes  40578  pm13.193  40743  2reu8i  43313  opeliun2xp  44382
  Copyright terms: Public domain W3C validator