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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	elabd.2	⊢ ( 𝜑 → 𝜒 )
	elabd.3	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
Assertion	elabd	⊢ ( 𝜑 → 𝐴 ∈ { 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		elabd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		elabd.2	⊢ ( 𝜑 → 𝜒 )
3		elabd.3	⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜒 ) )
4	3	elabg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜒 ) )
5	1 4	syl	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜒 ) )
6	2 5	mpbird	⊢ ( 𝜑 → 𝐴 ∈ { 𝑥 ∣ 𝜓 } )