Theorem sbequ12 2267

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)

Assertion

Ref	Expression
sbequ12	⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 2266	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2051	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 202	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 196  [wsb 2049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-sb 2050

This theorem is referenced by:  sbequ12r  2268  sbequ12a  2269  axc16ALT  2513  nfsb4t  2536  sbco2  2562  sb8  2571  sb8e  2572  sbal1  2608  clelab  2897  sbab  2899  cbvralf  3314  cbvralsv  3331  cbvrexsv  3332  cbvrab  3348  sbhypf  3405  mob2  3538  reu2  3546  reu6  3547  sbcralt  3660  sbcreu  3664  cbvreucsf  3716  cbvrabcsf  3717  csbif  4277  cbvopab1  4857  cbvopab1s  4859  cbvmptf  4882  cbvmpt  4883  opelopabsb  5118  csbopab  5141  csbopabgALT  5142  opeliunxp  5310  ralxpf  5407  cbviota  5999  csbiota  6024  f1ossf1o  6538  cbvriota  6764  csbriota  6766  onminex  7154  tfis  7201  findes  7243  abrexex2g  7291  opabex3d  7292  opabex3  7293  abrexex2OLD  7297  dfoprab4f  7375  uzind4s  11950  ac6sf2  29769  esumcvg  30488  bj-sbab  33120  wl-sb8t  33668  wl-sbalnae  33679  wl-ax11-lem8  33703  sbcrexgOLD  37875  pm13.193  39138  opeliun2xp  42639