Theorem sbequ12 1795

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

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

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 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534

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

This theorem is referenced by:  sbequ12r  1796  sbequ12a  1797  sbid  1798  ax16  1837  sb8h  1878  sb8eh  1879  sb8  1880  sb8e  1881  ax16ALT  1883  sbco  1997  sbcomxyyz  2001  sb9v  2007  sb6a  2017  mopick  2133  clelab  2332  sbab  2334  nfabdw  2368  cbvralf  2731  cbvrexf  2732  cbvralsv  2755  cbvrexsv  2756  cbvrab  2771  sbhypf  2824  mob2  2957  reu2  2965  reu6  2966  sbcralt  3079  sbcrext  3080  sbcralg  3081  sbcreug  3083  cbvreucsf  3162  cbvrabcsf  3163  cbvopab1  4125  cbvopab1s  4127  csbopabg  4130  cbvmptf  4146  cbvmpt  4147  opelopabsb  4314  frind  4407  tfis  4639  findes  4659  opeliunxp  4738  ralxpf  4832  rexxpf  4833  cbviota  5246  csbiotag  5273  cbvriota  5923  csbriotag  5925  abrexex2g  6218  opabex3d  6219  opabex3  6220  abrexex2  6222  dfoprab4f  6292  finexdc  7014  ssfirab  7048  uzind4s  9731  zsupcllemstep  10394  bezoutlemmain  12394  nnwosdc  12435  cbvrald  15863  bj-bdfindes  16023  bj-findes  16055