Theorem sbequ12 2252

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 2249	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2250	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 212	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbequ12r  2253  sbequ12a  2255  sb8ef  2353  sbbib  2359  axc16ALT  2487  nfsb4t  2497  sbco2  2509  sb8  2515  sb8e  2516  sbal1  2526  sbal2  2527  sbab  2875  cbvrexsvw  3282  cbvralsvwOLD  3283  cbvralsvwOLDOLD  3284  cbvrexsvwOLD  3285  cbvralf  3325  cbvralsv  3331  cbvrexsv  3332  cbvrabwOLD  3433  cbvrab  3437  sbhypfOLD  3502  mob2  3677  reu2  3687  reu6  3688  sbcralt  3826  sbcreu  3830  cbvrabcsfw  3894  cbvreucsf  3897  cbvrabcsf  3898  csbif  4536  cbvopab1  5169  cbvopab1g  5170  cbvopab1s  5172  cbvmptf  5195  cbvmptfg  5196  csbopab  5502  csbopabgALT  5503  opeliunxp  5690  opeliun2xp  5691  ralxpf  5793  cbviotaw  6449  cbviota  6451  csbiota  6479  f1ossf1o  7066  cbvriotaw  7319  cbvriota  7323  csbriota  7325  onminex  7742  tfis  7795  findes  7840  abrexex2g  7906  opabex3d  7907  opabex3rd  7908  opabex3  7909  dfoprab4f  7998  uzind4s  12827  ac6sf2  32581  esumcvg  34055  wl-sb8t  37528  wl-sbalnae  37538  wl-ax11-lem8  37568  sbcrexgOLD  42761  scottabes  44218  pm13.193  44387  2reu8i  47101  ichnfimlem  47451