Theorem sbequ12 1745

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

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

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 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488

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

This theorem is referenced by:  sbequ12r  1746  sbequ12a  1747  sbid  1748  ax16  1786  sb8h  1827  sb8eh  1828  sb8  1829  sb8e  1830  ax16ALT  1832  sbco  1942  sbcomxyyz  1946  sb9v  1954  sb6a  1964  mopick  2078  clelab  2266  sbab  2268  cbvralf  2651  cbvrexf  2652  cbvralsv  2671  cbvrexsv  2672  cbvrab  2687  sbhypf  2738  mob2  2868  reu2  2876  reu6  2877  sbcralt  2989  sbcrext  2990  sbcralg  2991  sbcreug  2993  cbvreucsf  3069  cbvrabcsf  3070  cbvopab1  4009  cbvopab1s  4011  csbopabg  4014  cbvmptf  4030  cbvmpt  4031  opelopabsb  4190  frind  4282  tfis  4505  findes  4525  opeliunxp  4602  ralxpf  4693  rexxpf  4694  cbviota  5101  csbiotag  5124  cbvriota  5748  csbriotag  5750  abrexex2g  6026  opabex3d  6027  opabex3  6028  abrexex2  6030  dfoprab4f  6099  finexdc  6804  ssfirab  6830  uzind4s  9412  zsupcllemstep  11674  bezoutlemmain  11722  cbvrald  13166  bj-bdfindes  13318  bj-findes  13350