Theorem sbequ12 865

Description: An equality theorem for substitution.

Assertion

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

Proof of Theorem sbequ12

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

Syntax hints:   → wi 2   ↔ wb 127   = weq 797  [wsb 852

This theorem is referenced by:  sbequ12r 866  sbequ12a 867  sbid 868  sbco 910  sbidm 912  sbco2 913  sbcom 916  sb5 988  sb6 989  sb6a 990  sbcom2 992  sbal1 996  mopick 1054  clelab 1187  sbab 1188  reu2 1338  vsbcint 1438  sbralie 1439  elrabsf 1456  iunrab 2022  opabid 2099  cbvopab1s 2107  opabsb 2114  tfis 2245  findes 2400  tfinds 2401  tfindes 2404  abrexex2 2915

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org