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  2024  sbcomxyyz  2028  sb9v  2034  sb6a  2044  mopick  2161  clelab  2362  sbab  2364  nfabdw  2405  cbvralf  2771  cbvrexf  2772  cbvralsv  2796  cbvrexsv  2797  cbvrab  2813  sbhypf  2866  mob2  3000  reu2  3008  reu6  3009  sbcralt  3122  sbcrext  3123  sbcralg  3124  sbcreug  3126  cbvreucsf  3206  cbvrabcsf  3207  cbvopab1  4188  cbvopab1s  4190  csbopabg  4193  cbvmptf  4209  cbvmpt  4210  opelopabsb  4383  frind  4478  tfis  4710  findes  4730  opeliunxp  4810  ralxpf  4906  rexxpf  4907  cbviota  5322  csbiotag  5350  cbvriota  6023  csbriotag  6025  abrexex2g  6322  opabex3d  6323  opabex3  6324  abrexex2  6326  dfoprab4f  6400  modom  7074  finexdc  7173  ssfirab  7210  uzind4s  9940  zsupcllemstep  10611  bezoutlemmain  12719  nnwosdc  12760  cbvrald  16686  bj-bdfindes  16845  bj-findes  16877