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

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

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2257 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 2048 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 202 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  [wsb 2046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-sb 2047
This theorem is referenced by:  sbequ12r  2259  sbequ12a  2260  axc16ALT  2503  nfsb4t  2526  sbco2  2552  sb8  2561  sb8e  2562  sbal1  2597  clelab  2886  sbab  2888  cbvralf  3304  cbvralsv  3321  cbvrexsv  3322  cbvrab  3338  sbhypf  3393  mob2  3527  reu2  3535  reu6  3536  sbcralt  3651  sbcreu  3656  cbvreucsf  3708  cbvrabcsf  3709  csbif  4282  cbvopab1  4875  cbvopab1s  4877  cbvmptf  4900  cbvmpt  4901  opelopabsb  5135  csbopab  5158  csbopabgALT  5159  opeliunxp  5327  ralxpf  5424  cbviota  6017  csbiota  6042  cbvriota  6784  csbriota  6786  onminex  7172  tfis  7219  findes  7261  abrexex2g  7309  opabex3d  7310  opabex3  7311  abrexex2OLD  7315  dfoprab4f  7393  uzind4s  11941  ac6sf2  29738  esumcvg  30457  bj-sbab  33090  wl-sb8t  33646  wl-sbalnae  33658  wl-ax11-lem8  33682  sbcrexgOLD  37851  pm13.193  39114  opeliun2xp  42621
  Copyright terms: Public domain W3C validator