Mathbox for Andrew Salmon |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > pm13.13a | Structured version Visualization version GIF version |
Description: One result of theorem *13.13 in [WhiteheadRussell] p. 178. A note on the section - to make the theorems more usable, and because inequality is notation for set theory (it is not defined in the predicate calculus section), this section will use classes instead of sets. (Contributed by Andrew Salmon, 3-Jun-2011.) |
Ref | Expression |
---|---|
pm13.13a | ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbceq1a 3726 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑)) | |
2 | 1 | biimpac 479 | 1 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → [𝐴 / 𝑥]𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 [wsbc 3715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-12 2171 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-sbc 3716 |
This theorem is referenced by: pm13.194 42011 |
Copyright terms: Public domain | W3C validator |