Metamath Proof Explorer

Theorem ralab2

Description: Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by GG, 1-Dec-2023)

		Ref	Expression
	Hypothesis	ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
	Assertion	ralab2	$⊢ \forall x \in \{y \| φ\} ψ \leftrightarrow \forall y (φ \to χ)$

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	$⊢ x = y \to (ψ \leftrightarrow χ)$
2		df-ral	$⊢ \forall x \in \{y \| φ\} ψ \leftrightarrow \forall x (x \in \{y \| φ\} \to ψ)$
3		nfsab1	$⊢ Ⅎ y x \in \{y \| φ\}$
4		nfv	$⊢ Ⅎ y ψ$
5	3 4	nfim	$⊢ Ⅎ y (x \in \{y \| φ\} \to ψ)$
6		nfv	$⊢ Ⅎ x (φ \to χ)$
7		eleq1ab	$⊢ x = y \to (x \in \{y \| φ\} \leftrightarrow y \in \{y \| φ\})$
8		abid	$⊢ y \in \{y \| φ\} \leftrightarrow φ$
9	7 8	bitrdi	$⊢ x = y \to (x \in \{y \| φ\} \leftrightarrow φ)$
10	9 1	imbi12d	$⊢ x = y \to ((x \in \{y \| φ\} \to ψ) \leftrightarrow (φ \to χ))$
11	5 6 10	cbvalv1	$⊢ \forall x (x \in \{y \| φ\} \to ψ) \leftrightarrow \forall y (φ \to χ)$
12	2 11	bitri	$⊢ \forall x \in \{y \| φ\} ψ \leftrightarrow \forall y (φ \to χ)$