This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The universal class rabab
Description: A class abstraction restricted to the universe is unrestricted.
(Contributed by NM , 27-Dec-2004) (Proof shortened by Andrew Salmon , 8-Jun-2011)
Ref
Expression
Assertion
rabab ⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ 𝜑 }
Proof
Step
Hyp
Ref
Expression
1
df-rab ⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
2
vex ⊢ 𝑥 ∈ V
3
2
biantrur ⊢ ( 𝜑 ↔ ( 𝑥 ∈ V ∧ 𝜑 ) )
4
3
abbii ⊢ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
5
1 4
eqtr4i ⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ 𝜑 }