This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-se

Description: Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014)

Ref Expression
Assertion df-se ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ⊢ 𝑅
1 cA ⊢ 𝐴
2 1 0 wse ⊢ 𝑅 Se 𝐴
3 vx ⊢ 𝑥
4 vy ⊢ 𝑦
5 4 cv ⊢ 𝑦
6 3 cv ⊢ 𝑥
7 5 6 0 wbr ⊢ 𝑦 𝑅 𝑥
8 7 4 1 crab ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 }
9 cvv ⊢ V
10 8 9 wcel ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V
11 10 3 1 wral ⊢ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V
12 2 11 wb ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )