![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > sbequ | GIF version |
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.) |
Ref | Expression |
---|---|
sbequ | ⊢ (x = y → ([x / z]φ ↔ [y / z]φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequi 2059 | . 2 ⊢ (x = y → ([x / z]φ → [y / z]φ)) | |
2 | sbequi 2059 | . . 3 ⊢ (y = x → ([y / z]φ → [x / z]φ)) | |
3 | 2 | equcoms 1681 | . 2 ⊢ (x = y → ([y / z]φ → [x / z]φ)) |
4 | 1, 3 | impbid 183 | 1 ⊢ (x = y → ([x / z]φ ↔ [y / z]φ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 [wsb 1648 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 |
This theorem is referenced by: drsb2 2061 sbco2 2086 sb10f 2122 sb8eu 2222 cbvab 2471 cbvralf 2829 cbvreu 2833 cbvralsv 2846 cbvrexsv 2847 cbvrab 2857 cbvreucsf 3200 cbvrabcsf 3201 sbss 3659 cbviota 4344 sb8iota 4346 cbvopab1 4632 cbvmpt 5676 |
Copyright terms: Public domain | W3C validator |