Theorem sbequ12 1759

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

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

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 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498

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

This theorem is referenced by:  sbequ12r  1760  sbequ12a  1761  sbid  1762  ax16  1801  sb8h  1842  sb8eh  1843  sb8  1844  sb8e  1845  ax16ALT  1847  sbco  1956  sbcomxyyz  1960  sb9v  1966  sb6a  1976  mopick  2092  clelab  2292  sbab  2294  nfabdw  2327  cbvralf  2685  cbvrexf  2686  cbvralsv  2708  cbvrexsv  2709  cbvrab  2724  sbhypf  2775  mob2  2906  reu2  2914  reu6  2915  sbcralt  3027  sbcrext  3028  sbcralg  3029  sbcreug  3031  cbvreucsf  3109  cbvrabcsf  3110  cbvopab1  4055  cbvopab1s  4057  csbopabg  4060  cbvmptf  4076  cbvmpt  4077  opelopabsb  4238  frind  4330  tfis  4560  findes  4580  opeliunxp  4659  ralxpf  4750  rexxpf  4751  cbviota  5158  csbiotag  5181  cbvriota  5808  csbriotag  5810  abrexex2g  6088  opabex3d  6089  opabex3  6090  abrexex2  6092  dfoprab4f  6161  finexdc  6868  ssfirab  6899  uzind4s  9528  zsupcllemstep  11878  bezoutlemmain  11931  nnwosdc  11972  cbvrald  13669  bj-bdfindes  13831  bj-findes  13863