Theorem sbequ12 1785

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

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

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 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524

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

This theorem is referenced by:  sbequ12r  1786  sbequ12a  1787  sbid  1788  ax16  1827  sb8h  1868  sb8eh  1869  sb8  1870  sb8e  1871  ax16ALT  1873  sbco  1987  sbcomxyyz  1991  sb9v  1997  sb6a  2007  mopick  2123  clelab  2322  sbab  2324  nfabdw  2358  cbvralf  2721  cbvrexf  2722  cbvralsv  2745  cbvrexsv  2746  cbvrab  2761  sbhypf  2813  mob2  2944  reu2  2952  reu6  2953  sbcralt  3066  sbcrext  3067  sbcralg  3068  sbcreug  3070  cbvreucsf  3149  cbvrabcsf  3150  cbvopab1  4107  cbvopab1s  4109  csbopabg  4112  cbvmptf  4128  cbvmpt  4129  opelopabsb  4295  frind  4388  tfis  4620  findes  4640  opeliunxp  4719  ralxpf  4813  rexxpf  4814  cbviota  5225  csbiotag  5252  cbvriota  5891  csbriotag  5893  abrexex2g  6186  opabex3d  6187  opabex3  6188  abrexex2  6190  dfoprab4f  6260  finexdc  6972  ssfirab  7006  uzind4s  9681  zsupcllemstep  10336  bezoutlemmain  12190  nnwosdc  12231  cbvrald  15518  bj-bdfindes  15679  bj-findes  15711