Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Ordered-pair class abstractions (class builders)
nfopab
Metamath Proof Explorer
Description: Bound-variable hypothesis builder for class abstraction. (Contributed by NM , 1-Sep-1999) Remove disjoint variable conditions. (Revised by Andrew Salmon , 11-Jul-2011)
Ref
Expression
Hypothesis
nfopab.1
⊢ Ⅎ z φ
Assertion
nfopab
⊢ Ⅎ _ z x y | φ
Proof
Step
Hyp
Ref
Expression
1
nfopab.1
⊢ Ⅎ z φ
2
df-opab
⊢ x y | φ = w | ∃ x ∃ y w = x y ∧ φ
3
nfv
⊢ Ⅎ z w = x y
4
3 1
nfan
⊢ Ⅎ z w = x y ∧ φ
5
4
nfex
⊢ Ⅎ z ∃ y w = x y ∧ φ
6
5
nfex
⊢ Ⅎ z ∃ x ∃ y w = x y ∧ φ
7
6
nfab
⊢ Ⅎ _ z w | ∃ x ∃ y w = x y ∧ φ
8
2 7
nfcxfr
⊢ Ⅎ _ z x y | φ