Theorem sbequ12 1919

Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
sbequ12	⊢ (x = y → (φ ↔ [y / x]φ))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1918	. 2 ⊢ (x = y → (φ → [y / x]φ))
2		sbequ2 1650	. 2 ⊢ (x = y → ([y / x]φ → φ))
3	1, 2	impbid 183	1 ⊢ (x = y → (φ ↔ [y / x]φ))

Syntax hints:   → wi 4   ↔ wb 176  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-sb 1649

This theorem is referenced by:  sbequ12r  1920  sbequ12a  1921  sbid  1922  ax16ALT  2047  ax16ALT2  2048  nfsb4t  2080  sbco  2083  sbco2  2086  sbcom  2089  sbcom2  2114  sb6a  2116  sbal1  2126  mopick  2266  2mo  2282  2eu6  2289  clelab  2474  sbab  2476  cbvralf  2830  cbvralsv  2847  cbvrexsv  2848  cbvrab  2858  sbhypf  2905  mob2  3017  reu2  3025  reu6  3026  sbcralt  3119  sbcralg  3121  sbcrexg  3122  sbcreug  3123  cbvreucsf  3201  cbvrabcsf  3202  csbifg  3691  cbviota  4345  csbiotag  4372  cbvopab1  4633  cbvopab1s  4635  csbopabg  4638  opelopabsb  4698  opeliunxp  4821  ralxpf  4828  cbvmpt  5677