Theorem sbequ12 1177

Description: An equality theorem for substitution.

Assertion

Ref	Expression
sbequ12	|- (x = y -> (ph <-> [y / x]ph))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1174	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1175	. 2 |- (x = y -> ([y / x]ph -> ph))
3	1, 2	impbid 514	1 |- (x = y -> (ph <-> [y / x]ph))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953  [wsbc 1166

This theorem is referenced by:  sbequ12r 1178  sbequ12a 1179  sbid 1180  ax16 1205  sbco 1247  sbidm 1249  sbco2 1250  sbcom 1253  ax16ALT 1266  sbcom2 1329  sb6a 1332  sbal1 1341  mopick 1426  2mo 1440  2eu6 1447  clelab 1573  sbab 1575  moi 1915  reu2 1920  reu3 1921  sbhypf 1929  sbhyp 1930  sbralie 1931  elrabsf 1953  cbvralsv 1957  cbvrexsv 1958  csbabg 2033  iunrab 2586  cbvopab1s 2665  opabid 2799  opabsb 2804  tfis 3117  findes 3150  tfinds 3151  tfindes 3154  ralxpf 3210  abrexex2 3856  uzind4s 6384  cau3i 6851

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 970

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168

Copyright terms: Public domain