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

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

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2108 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 1880 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 202 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  [wsb 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-sb 1879
This theorem is referenced by:  sbequ12r  2110  sbequ12a  2111  axc16ALT  2364  nfsb4t  2387  sbco2  2413  sb8  2422  sb8e  2423  sbal1  2458  clelab  2746  sbab  2748  cbvralf  3160  cbvralsv  3177  cbvrexsv  3178  cbvrab  3193  sbhypf  3248  mob2  3380  reu2  3388  reu6  3389  sbcralt  3504  sbcreu  3509  cbvreucsf  3560  cbvrabcsf  3561  csbif  4129  cbvopab1  4714  cbvopab1s  4716  cbvmptf  4739  cbvmpt  4740  opelopabsb  4975  csbopab  4998  csbopabgALT  4999  opeliunxp  5160  ralxpf  5257  cbviota  5844  csbiota  5869  cbvriota  6606  csbriota  6608  onminex  6992  tfis  7039  findes  7081  abrexex2g  7129  opabex3d  7130  opabex3  7131  abrexex2OLD  7135  dfoprab4f  7211  uzind4s  11733  ac6sf2  29401  esumcvg  30122  bj-sbab  32759  wl-sb8t  33304  wl-sbalnae  33316  wl-ax11-lem8  33340  sbcrexgOLD  37168  pm13.193  38432  opeliun2xp  41876
  Copyright terms: Public domain W3C validator