Metamath Proof Explorer

Theorem dfse2

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

Ref Expression
Assertion dfse2 ${⊢}{R}\mathrm{Se}{A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{A}\cap {{R}}^{-1}\left[\left\{{x}\right\}\right]\in \mathrm{V}$

Proof

Step Hyp Ref Expression
1 df-se ${⊢}{R}\mathrm{Se}{A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{y}{R}{x}\right\}\in \mathrm{V}$
2 dfrab3 ${⊢}\left\{{y}\in {A}|{y}{R}{x}\right\}={A}\cap \left\{{y}|{y}{R}{x}\right\}$
3 iniseg ${⊢}{x}\in \mathrm{V}\to {{R}}^{-1}\left[\left\{{x}\right\}\right]=\left\{{y}|{y}{R}{x}\right\}$
4 3 elv ${⊢}{{R}}^{-1}\left[\left\{{x}\right\}\right]=\left\{{y}|{y}{R}{x}\right\}$
5 4 ineq2i ${⊢}{A}\cap {{R}}^{-1}\left[\left\{{x}\right\}\right]={A}\cap \left\{{y}|{y}{R}{x}\right\}$
6 2 5 eqtr4i ${⊢}\left\{{y}\in {A}|{y}{R}{x}\right\}={A}\cap {{R}}^{-1}\left[\left\{{x}\right\}\right]$
7 6 eleq1i ${⊢}\left\{{y}\in {A}|{y}{R}{x}\right\}\in \mathrm{V}↔{A}\cap {{R}}^{-1}\left[\left\{{x}\right\}\right]\in \mathrm{V}$
8 7 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {A}|{y}{R}{x}\right\}\in \mathrm{V}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{A}\cap {{R}}^{-1}\left[\left\{{x}\right\}\right]\in \mathrm{V}$
9 1 8 bitri ${⊢}{R}\mathrm{Se}{A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{A}\cap {{R}}^{-1}\left[\left\{{x}\right\}\right]\in \mathrm{V}$