Theorem sbequ12 1179

Description: An equality theorem for substitution.

Assertion

Ref	Expression
sbequ12	⊢ (x = y → (φ ↔ [y / x]φ))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1176	. 2 ⊢ (x = y → (φ → [y / x]φ))
2		sbequ2 1177	. 2 ⊢ (x = y → ([y / x]φ → φ))
3	1, 2	impbid 515	1 ⊢ (x = y → (φ ↔ [y / x]φ))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 954  [wsbc 1168

This theorem is referenced by:  sbequ12r 1180  sbequ12a 1181  sbid 1182  ax16 1207  sbco 1250  sbidm 1252  sbco2 1253  sbcom 1256  ax16ALT 1269  sbcom2 1332  sb6a 1335  sbal1 1344  mopick 1431  2mo 1445  2eu6 1452  clelab 1578  sbab 1580  moi2 1920  moi 1921  reu2 1926  reu3 1927  sbhypf 1935  sbhyp 1936  sbralie 1937  elrabsf 1959  cbvralsv 1963  cbvrexsv 1964  csbabg 2039  iunrab 2592  cbvopab1s 2671  opabid 2807  opabsb 2812  tfis 3127  findes 3160  tfinds 3161  tfindes 3164  ralxpf 3220  abrexex2 3873  uzind4s 6404  cau3i 6871

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain