Theorem sbequ 1889

Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem sbequ

Step	Hyp	Ref	Expression
1		sbequi 1888	. 2 |- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
2		sbequi 1888	. . 3 |- ( y = x -> ( [ y / z ] ph -> [ x / z ] ph ) )
3	2	equcoms 1756	. 2 |- ( x = y -> ( [ y / z ] ph -> [ x / z ] ph ) )
4	1, 3	impbid 129	1 |- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )

Syntax hints:   -> wi 4   <-> wb 105   [wsb 1811

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-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812

This theorem is referenced by:  drsb2  1890  sbco2vlem  2000  sbco2v  2004  sbco2yz  2019  sbcocom  2026  sb10f  2051  hbsb4  2068  nfsb4or  2077  sb8eu  2095  sb8euh  2105  cbvab  2360  cbvralf  2771  cbvrexf  2772  cbvreu  2778  cbvralsv  2796  cbvrexsv  2797  cbvrab  2813  cbvreucsf  3206  cbvrabcsf  3207  sbss  3621  disjiun  4109  cbvopab1  4188  cbvmpt  4210  tfis  4710  findes  4730  cbviota  5322  sb8iota  5325  cbvriota  6023  modom  7074  uzind4s  9940  bezoutlemmain  12719  cbvrald  16686  setindft  16861