New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ax-14 | GIF version |
Description: Axiom of Right Equality for Binary Predicate. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of an arbitrary binary predicate ∈, which we will use for the set membership relation when set theory is introduced. This axiom scheme is a sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose general form cannot be represented with our notation. Also appears as Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ax-14 | ⊢ (x = y → (z ∈ x → z ∈ y)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar x | |
2 | vy | . . 3 setvar y | |
3 | 1, 2 | weq 1643 | . 2 wff x = y |
4 | vz | . . . 4 setvar z | |
5 | 4, 1 | wel 1711 | . . 3 wff z ∈ x |
6 | 4, 2 | wel 1711 | . . 3 wff z ∈ y |
7 | 5, 6 | wi 4 | . 2 wff (z ∈ x → z ∈ y) |
8 | 3, 7 | wi 4 | 1 wff (x = y → (z ∈ x → z ∈ y)) |
Colors of variables: wff setvar class |
This axiom is referenced by: elequ2 1715 fv3 5341 |
Copyright terms: Public domain | W3C validator |