Theorem sbequ 1813

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 1812	. 2 |- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
2		sbequi 1812	. . 3 |- ( y = x -> ( [ y / z ] ph -> [ x / z ] ph ) )
3	2	equcoms 1685	. 2 |- ( x = y -> ( [ y / z ] ph -> [ x / z ] ph ) )
4	1, 3	impbid 128	1 |- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )

Syntax hints:   -> wi 4   <-> wb 104   [wsb 1736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737

This theorem is referenced by:  drsb2  1814  sbco2vlem  1918  sbco2v  1922  sbco2yz  1937  sbcocom  1944  sb10f  1971  hbsb4  1988  nfsb4or  1999  sb8eu  2013  sb8euh  2023  cbvab  2264  cbvralf  2651  cbvrexf  2652  cbvreu  2655  cbvralsv  2671  cbvrexsv  2672  cbvrab  2687  cbvreucsf  3069  cbvrabcsf  3070  sbss  3476  disjiun  3932  cbvopab1  4009  cbvmpt  4031  tfis  4505  findes  4525  cbviota  5101  sb8iota  5103  cbvriota  5748  uzind4s  9412  bezoutlemmain  11722  cbvrald  13166  setindft  13334