Theorem sbequ12 1702

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446

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

This theorem is referenced by:  sbequ12r  1703  sbequ12a  1704  sbid  1705  ax16  1742  sb8h  1783  sb8eh  1784  sb8  1785  sb8e  1786  ax16ALT  1788  sbco  1891  sbcomxyyz  1895  sb9v  1903  sb6a  1913  mopick  2027  clelab  2213  sbab  2215  cbvralf  2585  cbvrexf  2586  cbvralsv  2602  cbvrexsv  2603  cbvrab  2618  sbhypf  2669  mob2  2796  reu2  2804  reu6  2805  sbcralt  2916  sbcrext  2917  sbcralg  2918  sbcreug  2920  cbvreucsf  2993  cbvrabcsf  2994  cbvopab1  3917  cbvopab1s  3919  csbopabg  3922  cbvmptf  3938  cbvmpt  3939  opelopabsb  4096  frind  4188  tfis  4411  findes  4431  opeliunxp  4506  ralxpf  4595  rexxpf  4596  cbviota  4998  csbiotag  5021  cbvriota  5632  csbriotag  5634  abrexex2g  5905  opabex3d  5906  opabex3  5907  abrexex2  5909  dfoprab4f  5977  finexdc  6672  ssfirab  6697  uzind4s  9139  zsupcllemstep  11280  bezoutlemmain  11326  cbvrald  11961  bj-bdfindes  12117  bj-findes  12149