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 )