Theorem sbequ12 2247

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

Syntax hints:   → wi 4   ↔ wb 205  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069

This theorem is referenced by:  sbequ12r  2248  sbequ12a  2250  sb5OLD  2272  sb8v  2352  sb8ev  2353  sbbib  2359  axc16ALT  2493  nfsb4t  2503  sbco2  2515  sb8  2521  sb8e  2522  sbal1  2533  sbal2  2534  clelabOLD  2883  sbab  2885  nfabdwOLD  2930  cbvralfwOLD  3359  cbvralf  3361  cbvralsvw  3391  cbvrexsvw  3392  cbvralsv  3393  cbvrexsv  3394  cbvrabw  3414  cbvrab  3415  sbhypf  3481  mob2  3645  reu2  3655  reu6  3656  sbcralt  3801  sbcreu  3805  cbvrabcsfw  3872  cbvreucsf  3875  cbvrabcsf  3876  csbif  4513  cbvopab1  5145  cbvopab1g  5146  cbvopab1s  5148  cbvmptf  5179  cbvmptfg  5180  csbopab  5461  csbopabgALT  5462  opeliunxp  5645  ralxpf  5744  cbviotaw  6383  cbviota  6386  csbiota  6411  f1ossf1o  6982  cbvriotaw  7221  cbvriota  7226  csbriota  7228  onminex  7629  tfis  7676  findes  7723  abrexex2g  7780  opabex3d  7781  opabex3rd  7782  opabex3  7783  dfoprab4f  7869  uzind4s  12577  ac6sf2  30861  esumcvg  31954  wl-sb8t  35634  wl-sbalnae  35644  wl-ax11-lem8  35670  sbcrexgOLD  40523  scottabes  41749  pm13.193  41918  2reu8i  44492  ichnfimlem  44803  opeliun2xp  45556