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

Metamath Proof Explorer

Theorem kqfval

Description: Value of the function appearing in df-kq . (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqfval	$⊢ (J \in V \land A \in X) \to F (A) = \{y \in J \| A \in y\}$

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2		id	$⊢ A \in X \to A \in X$
3		rabexg	$⊢ J \in V \to \{y \in J \| A \in y\} \in V$
4		eleq1	$⊢ x = A \to (x \in y \leftrightarrow A \in y)$
5	4	rabbidv	$⊢ x = A \to \{y \in J \| x \in y\} = \{y \in J \| A \in y\}$
6	5 1	fvmptg	$⊢ (A \in X \land \{y \in J \| A \in y\} \in V) \to F (A) = \{y \in J \| A \in y\}$
7	2 3 6	syl2anr	$⊢ (J \in V \land A \in X) \to F (A) = \{y \in J \| A \in y\}$