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

Metamath Proof Explorer

Theorem dfse2

Description: Alternate definition of set-like relation. (Contributed by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dfse2 ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑥 } ) ) ∈ V )

Proof

Step Hyp Ref Expression
1 df-se ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V )
2 dfrab3 ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑥 } )
3 iniseg ⊢ ( 𝑥 ∈ V → ( ◡ 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑦 𝑅 𝑥 } )
4 3 elv ⊢ ( ◡ 𝑅 “ { 𝑥 } ) = { 𝑦 ∣ 𝑦 𝑅 𝑥 }
5 4 ineq2i ⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑥 } ) ) = ( 𝐴 ∩ { 𝑦 ∣ 𝑦 𝑅 𝑥 } )
6 2 5 eqtr4i ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑥 } ) )
7 6 eleq1i ⊢ ( { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ↔ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑥 } ) ) ∈ V )
8 7 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 } ∈ V ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑥 } ) ) ∈ V )
9 1 8 bitri ⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑥 } ) ) ∈ V )