Theorem sbequ12 1164

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 1161	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1162	. 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 1099  [wsbc 1153

This theorem is referenced by:  sbequ12r 1165  sbequ12a 1166  sbid 1167  ax16 1193  sbco 1236  sbidm 1238  sbco2 1239  sbcom 1242  sbcom2 1316  sb6a 1319  sbal1 1328  mopick 1410  2mo 1424  2eu6 1431  clelab 1557  sbab 1559  moi 1896  reu2 1901  reu3 1902  sbhypf 1910  sbhyp 1911  sbralie 1912  elrabsf 1934  cbvralsv 1938  cbvrexsv 1939  csbabg 2014  iunrab 2564  cbvopab1s 2643  opabid 2772  opabsb 2777  tfis 3090  findes 3123  tfinds 3124  tfindes 3127  ralxpf 3182  abrexex2 3810  uzind4s 6335  cau3i 6802

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155

Copyright terms: Public domain