Metamath Proof Explorer

Theorem wl-dfrabv

Description: Alternate definition of restricted class abstraction ( df-wl-rab ), when x and A are disjoint. (Contributed by Wolf Lammen, 29-May-2023)

		Ref	Expression
	Assertion	wl-dfrabv	$⊢ \{x : A \| φ\} = \{x \| (x \in A \land φ)\}$

Proof

Step	Hyp	Ref	Expression
1		wl-dfrabsb	$⊢ \{x : A \| φ\} = \{y \| (y \in A \land [y/ x] φ)\}$
2		clelsb3	$⊢ [z/ y] y \in A \leftrightarrow z \in A$
3		clelsb3	$⊢ [z/ x] x \in A \leftrightarrow z \in A$
4	2 3	bitr4i	$⊢ [z/ y] y \in A \leftrightarrow [z/ x] x \in A$
5		sbco2vv	$⊢ [z/ y] [y/ x] φ \leftrightarrow [z/ x] φ$
6	4 5	anbi12i	$⊢ ([z/ y] y \in A \land [z/ y] [y/ x] φ) \leftrightarrow ([z/ x] x \in A \land [z/ x] φ)$
7		df-clab	$⊢ z \in \{y \| (y \in A \land [y/ x] φ)\} \leftrightarrow [z/ y] (y \in A \land [y/ x] φ)$
8		sban	$⊢ [z/ y] (y \in A \land [y/ x] φ) \leftrightarrow ([z/ y] y \in A \land [z/ y] [y/ x] φ)$
9	7 8	bitri	$⊢ z \in \{y \| (y \in A \land [y/ x] φ)\} \leftrightarrow ([z/ y] y \in A \land [z/ y] [y/ x] φ)$
10		df-clab	$⊢ z \in \{x \| (x \in A \land φ)\} \leftrightarrow [z/ x] (x \in A \land φ)$
11		sban	$⊢ [z/ x] (x \in A \land φ) \leftrightarrow ([z/ x] x \in A \land [z/ x] φ)$
12	10 11	bitri	$⊢ z \in \{x \| (x \in A \land φ)\} \leftrightarrow ([z/ x] x \in A \land [z/ x] φ)$
13	6 9 12	3bitr4i	$⊢ z \in \{y \| (y \in A \land [y/ x] φ)\} \leftrightarrow z \in \{x \| (x \in A \land φ)\}$
14	13	eqriv	$⊢ \{y \| (y \in A \land [y/ x] φ)\} = \{x \| (x \in A \land φ)\}$
15	1 14	eqtri	$⊢ \{x : A \| φ\} = \{x \| (x \in A \land φ)\}$