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	$$⊢\phi \to A\in V$$
	elabd.2	$$⊢\phi \to \chi$$
	elabd.3	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	elabd	$$⊢\phi \to A\in \left\{x|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		elabd.1	$$⊢\phi \to A\in V$$
2		elabd.2	$$⊢\phi \to \chi$$
3		elabd.3	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
4	3	elabg	$$⊢A\in V\to \left(A\in \left\{x|\psi \right\}\leftrightarrow \chi \right)$$
5	1 4	syl	$$⊢\phi \to \left(A\in \left\{x|\psi \right\}\leftrightarrow \chi \right)$$
6	2 5	mpbird	$$⊢\phi \to A\in \left\{x|\psi \right\}$$