Theorem sbequ12 1820

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

Syntax hints:   → wi 4   ↔ wb 105  [wsb 1811

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 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

This theorem depends on definitions:  df-bi 117  df-sb 1812

This theorem is referenced by:  sbequ12r  1821  sbequ12a  1822  sbid  1823  ax16  1862  sb8h  1903  sb8eh  1904  sb8  1905  sb8e  1906  ax16ALT  1908  sbco  2022  sbcomxyyz  2026  sb9v  2032  sb6a  2042  mopick  2159  clelab  2360  sbab  2362  nfabdw  2403  cbvralf  2769  cbvrexf  2770  cbvralsv  2794  cbvrexsv  2795  cbvrab  2811  sbhypf  2864  mob2  2997  reu2  3005  reu6  3006  sbcralt  3119  sbcrext  3120  sbcralg  3121  sbcreug  3123  cbvreucsf  3203  cbvrabcsf  3204  cbvopab1  4183  cbvopab1s  4185  csbopabg  4188  cbvmptf  4204  cbvmpt  4205  opelopabsb  4378  frind  4473  tfis  4705  findes  4725  opeliunxp  4805  ralxpf  4901  rexxpf  4902  cbviota  5317  csbiotag  5345  cbvriota  6015  csbriotag  6017  abrexex2g  6313  opabex3d  6314  opabex3  6315  abrexex2  6317  dfoprab4f  6387  modom  7061  finexdc  7160  ssfirab  7197  uzind4s  9922  zsupcllemstep  10589  bezoutlemmain  12694  nnwosdc  12735  cbvrald  16560  bj-bdfindes  16719  bj-findes  16751