Theorem sbequ12 2249

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063

This theorem is referenced by:  sbequ12r  2250  sbequ12a  2252  sb8fOLD  2355  sb8ef  2356  sbbib  2362  axc16ALT  2492  nfsb4t  2502  sbco2  2514  sb8  2520  sb8e  2521  sbal1  2531  sbal2  2532  sbab  2887  cbvrexsvw  3316  cbvralsvwOLD  3317  cbvralsvwOLDOLD  3318  cbvrexsvwOLD  3319  cbvralf  3358  cbvralsv  3364  cbvrexsv  3365  cbvrabwOLD  3472  cbvrab  3477  sbhypfOLD  3545  mob2  3724  reu2  3734  reu6  3735  sbcralt  3881  sbcreu  3885  cbvrabcsfw  3952  cbvreucsf  3955  cbvrabcsf  3956  csbif  4588  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvmptf  5257  cbvmptfg  5258  csbopab  5565  csbopabgALT  5566  opeliunxp  5756  ralxpf  5860  cbviotaw  6523  cbviota  6525  csbiota  6556  f1ossf1o  7148  cbvriotaw  7397  cbvriota  7401  csbriota  7403  onminex  7822  tfis  7876  findes  7923  abrexex2g  7988  opabex3d  7989  opabex3rd  7990  opabex3  7991  dfoprab4f  8080  uzind4s  12948  ac6sf2  32642  esumcvg  34067  wl-sb8t  37533  wl-sbalnae  37543  wl-ax11-lem8  37573  sbcrexgOLD  42773  scottabes  44238  pm13.193  44407  2reu8i  47063  ichnfimlem  47388  opeliun2xp  48178