Theorem sbequ12 1764

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

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

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 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503

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

This theorem is referenced by:  sbequ12r  1765  sbequ12a  1766  sbid  1767  ax16  1806  sb8h  1847  sb8eh  1848  sb8  1849  sb8e  1850  ax16ALT  1852  sbco  1961  sbcomxyyz  1965  sb9v  1971  sb6a  1981  mopick  2097  clelab  2296  sbab  2298  nfabdw  2331  cbvralf  2689  cbvrexf  2690  cbvralsv  2712  cbvrexsv  2713  cbvrab  2728  sbhypf  2779  mob2  2910  reu2  2918  reu6  2919  sbcralt  3031  sbcrext  3032  sbcralg  3033  sbcreug  3035  cbvreucsf  3113  cbvrabcsf  3114  cbvopab1  4062  cbvopab1s  4064  csbopabg  4067  cbvmptf  4083  cbvmpt  4084  opelopabsb  4245  frind  4337  tfis  4567  findes  4587  opeliunxp  4666  ralxpf  4757  rexxpf  4758  cbviota  5165  csbiotag  5191  cbvriota  5819  csbriotag  5821  abrexex2g  6099  opabex3d  6100  opabex3  6101  abrexex2  6103  dfoprab4f  6172  finexdc  6880  ssfirab  6911  uzind4s  9549  zsupcllemstep  11900  bezoutlemmain  11953  nnwosdc  11994  cbvrald  13823  bj-bdfindes  13984  bj-findes  14016