Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
reloprab
Next ⟩
oprabv
Metamath Proof Explorer
Ascii
Unicode
Theorem
reloprab
Description:
An operation class abstraction is a relation.
(Contributed by
NM
, 16-Jun-2004)
Ref
Expression
Assertion
reloprab
⊢
Rel
⁡
x
y
z
|
φ
Proof
Step
Hyp
Ref
Expression
1
dfoprab2
⊢
x
y
z
|
φ
=
w
z
|
∃
x
∃
y
w
=
x
y
∧
φ
2
1
relopabi
⊢
Rel
⁡
x
y
z
|
φ