Theorem sbequ12 1771

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

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

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 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

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

This theorem is referenced by:  sbequ12r  1772  sbequ12a  1773  sbid  1774  ax16  1813  sb8h  1854  sb8eh  1855  sb8  1856  sb8e  1857  ax16ALT  1859  sbco  1968  sbcomxyyz  1972  sb9v  1978  sb6a  1988  mopick  2104  clelab  2303  sbab  2305  nfabdw  2338  cbvralf  2697  cbvrexf  2698  cbvralsv  2720  cbvrexsv  2721  cbvrab  2736  sbhypf  2787  mob2  2918  reu2  2926  reu6  2927  sbcralt  3040  sbcrext  3041  sbcralg  3042  sbcreug  3044  cbvreucsf  3122  cbvrabcsf  3123  cbvopab1  4077  cbvopab1s  4079  csbopabg  4082  cbvmptf  4098  cbvmpt  4099  opelopabsb  4261  frind  4353  tfis  4583  findes  4603  opeliunxp  4682  ralxpf  4774  rexxpf  4775  cbviota  5184  csbiotag  5210  cbvriota  5841  csbriotag  5843  abrexex2g  6121  opabex3d  6122  opabex3  6123  abrexex2  6125  dfoprab4f  6194  finexdc  6902  ssfirab  6933  uzind4s  9590  zsupcllemstep  11946  bezoutlemmain  11999  nnwosdc  12040  cbvrald  14543  bj-bdfindes  14704  bj-findes  14736