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

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

Proof of Theorem sbequ12
StepHypRef Expression
1 sbequ1 2107 . 2 (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2 sbequ2 1879 . 2 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑𝜑))
31, 2impbid 202 1 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  [wsb 1877
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-sb 1878
This theorem is referenced by:  sbequ12r  2109  sbequ12a  2110  axc16ALT  2365  nfsb4t  2388  sbco2  2414  sb8  2423  sb8e  2424  sbal1  2459  clelab  2745  sbab  2747  cbvralf  3153  cbvralsv  3170  cbvrexsv  3171  cbvrab  3184  sbhypf  3239  mob2  3368  reu2  3376  reu6  3377  sbcralt  3492  sbcreu  3497  cbvreucsf  3548  cbvrabcsf  3549  csbif  4110  rabasiun  4489  cbvopab1  4685  cbvopab1s  4687  cbvmptf  4708  cbvmpt  4709  opelopabsb  4945  csbopab  4968  csbopabgALT  4969  opeliunxp  5131  ralxpf  5228  cbviota  5815  csbiota  5840  cbvriota  6575  csbriota  6577  onminex  6954  tfis  7001  findes  7043  abrexex2g  7090  opabex3d  7091  opabex3  7092  abrexex2  7094  dfoprab4f  7171  uzind4s  11692  ac6sf2  29272  esumcvg  29929  bj-sbab  32427  wl-sb8t  32965  wl-sbalnae  32977  wl-ax11-lem8  33001  sbcrexgOLD  36829  pm13.193  38094  opeliun2xp  41399
  Copyright terms: Public domain W3C validator