Theorem sbequ12 1782

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

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

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 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521

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

This theorem is referenced by:  sbequ12r  1783  sbequ12a  1784  sbid  1785  ax16  1824  sb8h  1865  sb8eh  1866  sb8  1867  sb8e  1868  ax16ALT  1870  sbco  1984  sbcomxyyz  1988  sb9v  1994  sb6a  2004  mopick  2120  clelab  2319  sbab  2321  nfabdw  2355  cbvralf  2718  cbvrexf  2719  cbvralsv  2742  cbvrexsv  2743  cbvrab  2758  sbhypf  2809  mob2  2940  reu2  2948  reu6  2949  sbcralt  3062  sbcrext  3063  sbcralg  3064  sbcreug  3066  cbvreucsf  3145  cbvrabcsf  3146  cbvopab1  4102  cbvopab1s  4104  csbopabg  4107  cbvmptf  4123  cbvmpt  4124  opelopabsb  4290  frind  4383  tfis  4615  findes  4635  opeliunxp  4714  ralxpf  4808  rexxpf  4809  cbviota  5220  csbiotag  5247  cbvriota  5884  csbriotag  5886  abrexex2g  6172  opabex3d  6173  opabex3  6174  abrexex2  6176  dfoprab4f  6246  finexdc  6958  ssfirab  6990  uzind4s  9655  zsupcllemstep  12082  bezoutlemmain  12135  nnwosdc  12176  cbvrald  15280  bj-bdfindes  15441  bj-findes  15473