Theorem sbequ12 1824

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  [wsb 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

This proof depends on definitions:  df-bi 117  df-sb 1816

This theorem is used by:  sbequ12r  1825  sbequ12a  1826  sbid  1827  ax16  1866  sb8h  1907  sb8eh  1908  sb8  1909  sb8e  1910  ax16ALT  1912  sbco  2028  sbcomxyyz  2032  sb9v  2038  sb6a  2048  mopick  2165  clelab  2366  sbab  2368  nfabdw  2411  cbvralf  2777  cbvrexf  2778  cbvralsv  2802  cbvrexsv  2803  cbvrab  2819  sbhypf  2872  mob2  3006  reu2  3014  reu6  3015  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcreug  3132  cbvreucsf  3212  cbvrabcsf  3213  cbvopab1  4204  cbvopab1s  4206  csbopabg  4209  cbvmptf  4225  cbvmpt  4226  opelopabsb  4402  frind  4497  tfis  4730  findes  4750  opeliunxp  4830  ralxpf  4926  rexxpf  4927  cbviota  5342  csbiotag  5370  cbvriota  6050  csbriotag  6052  abrexex2g  6349  opabex3d  6350  opabex3  6351  abrexex2  6353  dfoprab4f  6427  modom  7108  finexdc  7207  ssfirab  7244  uzind4s  9990  zsupcllemstep  10662  bezoutlemmain  12775  nnwosdc  12816  cbvrald  16816  bj-bdfindes  16975  bj-findes  17007