Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
Axiom scheme ax-9 (Right Equality for Binary Predicate)
elequ2
Next ⟩
elsb4
Metamath Proof Explorer
Ascii
Unicode
Theorem
elequ2
Description:
An identity law for the non-logical predicate.
(Contributed by
NM
, 21-Jun-1993)
Ref
Expression
Assertion
elequ2
⊢
x
=
y
→
z
∈
x
↔
z
∈
y
Proof
Step
Hyp
Ref
Expression
1
ax9
⊢
x
=
y
→
z
∈
x
→
z
∈
y
2
ax9
⊢
y
=
x
→
z
∈
y
→
z
∈
x
3
2
equcoms
⊢
x
=
y
→
z
∈
y
→
z
∈
x
4
1
3
impbid
⊢
x
=
y
→
z
∈
x
↔
z
∈
y