Theorem sbequ12 1817

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

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

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 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556

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

This theorem is referenced by:  sbequ12r  1818  sbequ12a  1819  sbid  1820  ax16  1859  sb8h  1900  sb8eh  1901  sb8  1902  sb8e  1903  ax16ALT  1905  sbco  2019  sbcomxyyz  2023  sb9v  2029  sb6a  2039  mopick  2156  clelab  2355  sbab  2357  nfabdw  2391  cbvralf  2756  cbvrexf  2757  cbvralsv  2781  cbvrexsv  2782  cbvrab  2797  sbhypf  2850  mob2  2983  reu2  2991  reu6  2992  sbcralt  3105  sbcrext  3106  sbcralg  3107  sbcreug  3109  cbvreucsf  3189  cbvrabcsf  3190  cbvopab1  4156  cbvopab1s  4158  csbopabg  4161  cbvmptf  4177  cbvmpt  4178  opelopabsb  4347  frind  4442  tfis  4674  findes  4694  opeliunxp  4773  ralxpf  4867  rexxpf  4868  cbviota  5282  csbiotag  5310  cbvriota  5965  csbriotag  5967  abrexex2g  6263  opabex3d  6264  opabex3  6265  abrexex2  6267  dfoprab4f  6337  finexdc  7060  ssfirab  7094  uzind4s  9781  zsupcllemstep  10444  bezoutlemmain  12514  nnwosdc  12555  cbvrald  16110  bj-bdfindes  16270  bj-findes  16302