Theorem sbequ12 1782

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

Syntax hints:   → wi 4   ↔ wb 105  [wsb 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521

This theorem depends on definitions:  df-bi 117  df-sb 1774

This theorem is referenced by:  sbequ12r  1783  sbequ12a  1784  sbid  1785  ax16  1824  sb8h  1865  sb8eh  1866  sb8  1867  sb8e  1868  ax16ALT  1870  sbco  1984  sbcomxyyz  1988  sb9v  1994  sb6a  2004  mopick  2120  clelab  2319  sbab  2321  nfabdw  2355  cbvralf  2718  cbvrexf  2719  cbvralsv  2742  cbvrexsv  2743  cbvrab  2758  sbhypf  2810  mob2  2941  reu2  2949  reu6  2950  sbcralt  3063  sbcrext  3064  sbcralg  3065  sbcreug  3067  cbvreucsf  3146  cbvrabcsf  3147  cbvopab1  4103  cbvopab1s  4105  csbopabg  4108  cbvmptf  4124  cbvmpt  4125  opelopabsb  4291  frind  4384  tfis  4616  findes  4636  opeliunxp  4715  ralxpf  4809  rexxpf  4810  cbviota  5221  csbiotag  5248  cbvriota  5885  csbriotag  5887  abrexex2g  6174  opabex3d  6175  opabex3  6176  abrexex2  6178  dfoprab4f  6248  finexdc  6960  ssfirab  6992  uzind4s  9658  zsupcllemstep  12085  bezoutlemmain  12138  nnwosdc  12179  cbvrald  15350  bj-bdfindes  15511  bj-findes  15543