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  1980  sbcomxyyz  1984  sb9v  1990  sb6a  2000  mopick  2116  clelab  2315  sbab  2317  nfabdw  2351  cbvralf  2710  cbvrexf  2711  cbvralsv  2734  cbvrexsv  2735  cbvrab  2750  sbhypf  2801  mob2  2932  reu2  2940  reu6  2941  sbcralt  3054  sbcrext  3055  sbcralg  3056  sbcreug  3058  cbvreucsf  3136  cbvrabcsf  3137  cbvopab1  4091  cbvopab1s  4093  csbopabg  4096  cbvmptf  4112  cbvmpt  4113  opelopabsb  4278  frind  4370  tfis  4600  findes  4620  opeliunxp  4699  ralxpf  4791  rexxpf  4792  cbviota  5201  csbiotag  5228  cbvriota  5861  csbriotag  5863  abrexex2g  6144  opabex3d  6145  opabex3  6146  abrexex2  6148  dfoprab4f  6217  finexdc  6929  ssfirab  6961  uzind4s  9619  zsupcllemstep  11977  bezoutlemmain  12030  nnwosdc  12071  cbvrald  14993  bj-bdfindes  15154  bj-findes  15186