Theorem sbequ12 1744

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

Assertion

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

Proof of Theorem sbequ12

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

Syntax hints:   → wi 4   ↔ wb 104  [wsb 1735

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487

This theorem depends on definitions:  df-bi 116  df-sb 1736

This theorem is referenced by:  sbequ12r  1745  sbequ12a  1746  sbid  1747  ax16  1785  sb8h  1826  sb8eh  1827  sb8  1828  sb8e  1829  ax16ALT  1831  sbco  1939  sbcomxyyz  1943  sb9v  1951  sb6a  1961  mopick  2075  clelab  2263  sbab  2265  cbvralf  2646  cbvrexf  2647  cbvralsv  2663  cbvrexsv  2664  cbvrab  2679  sbhypf  2730  mob2  2859  reu2  2867  reu6  2868  sbcralt  2980  sbcrext  2981  sbcralg  2982  sbcreug  2984  cbvreucsf  3059  cbvrabcsf  3060  cbvopab1  3996  cbvopab1s  3998  csbopabg  4001  cbvmptf  4017  cbvmpt  4018  opelopabsb  4177  frind  4269  tfis  4492  findes  4512  opeliunxp  4589  ralxpf  4680  rexxpf  4681  cbviota  5088  csbiotag  5111  cbvriota  5733  csbriotag  5735  abrexex2g  6011  opabex3d  6012  opabex3  6013  abrexex2  6015  dfoprab4f  6084  finexdc  6789  ssfirab  6815  uzind4s  9378  zsupcllemstep  11627  bezoutlemmain  11675  cbvrald  12984  bj-bdfindes  13136  bj-findes  13168