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

Metamath Proof Explorer

Theorem elabd

Description: Explicit demonstration the class { x | ps } is not empty by the example A . (Contributed by RP, 12-Aug-2020) (Revised by AV, 23-Mar-2024)

	Ref	Expression
Hypotheses	elabd.1	$⊢ φ \to A \in V$
	elabd.2	$⊢ φ \to χ$
	elabd.3	$⊢ x = A \to (ψ \leftrightarrow χ)$
Assertion	elabd	$⊢ φ \to A \in \{x \| ψ\}$

Proof

Step	Hyp	Ref	Expression
1		elabd.1	$⊢ φ \to A \in V$
2		elabd.2	$⊢ φ \to χ$
3		elabd.3	$⊢ x = A \to (ψ \leftrightarrow χ)$
4	3	elabg	$⊢ A \in V \to (A \in \{x \| ψ\} \leftrightarrow χ)$
5	1 4	syl	$⊢ φ \to (A \in \{x \| ψ\} \leftrightarrow χ)$
6	2 5	mpbird	$⊢ φ \to A \in \{x \| ψ\}$