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  2798  sbhypf  2851  mob2  2984  reu2  2992  reu6  2993  sbcralt  3106  sbcrext  3107  sbcralg  3108  sbcreug  3110  cbvreucsf  3190  cbvrabcsf  3191  cbvopab1  4160  cbvopab1s  4162  csbopabg  4165  cbvmptf  4181  cbvmpt  4182  opelopabsb  4352  frind  4447  tfis  4679  findes  4699  opeliunxp  4779  ralxpf  4874  rexxpf  4875  cbviota  5289  csbiotag  5317  cbvriota  5978  csbriotag  5980  abrexex2g  6277  opabex3d  6278  opabex3  6279  abrexex2  6281  dfoprab4f  6351  modom  6989  finexdc  7085  ssfirab  7121  uzind4s  9814  zsupcllemstep  10479  bezoutlemmain  12559  nnwosdc  12600  cbvrald  16320  bj-bdfindes  16480  bj-findes  16512