Theorem sbequ 1863

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 1862	. 2 |- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
2		sbequi 1862	. . 3 |- ( y = x -> ( [ y / z ] ph -> [ x / z ] ph ) )
3	2	equcoms 1731	. 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 1785

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786

This theorem is referenced by:  drsb2  1864  sbco2vlem  1972  sbco2v  1976  sbco2yz  1991  sbcocom  1998  sb10f  2023  hbsb4  2040  nfsb4or  2049  sb8eu  2067  sb8euh  2077  cbvab  2329  cbvralf  2730  cbvrexf  2731  cbvreu  2736  cbvralsv  2754  cbvrexsv  2755  cbvrab  2770  cbvreucsf  3158  cbvrabcsf  3159  sbss  3568  disjiun  4040  cbvopab1  4118  cbvmpt  4140  tfis  4632  findes  4652  cbviota  5238  sb8iota  5240  cbvriota  5912  uzind4s  9713  bezoutlemmain  12352  cbvrald  15761  setindft  15938