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

Metamath Proof Explorer

Theorem elabf

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 1-Aug-1994) (Revised by Mario Carneiro, 12-Oct-2016)

	Ref	Expression
Hypotheses	elabf.1	⊢ Ⅎ 𝑥 𝜓
	elabf.2	⊢ 𝐴 ∈ V
	elabf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	elabf	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		elabf.1	⊢ Ⅎ 𝑥 𝜓
2		elabf.2	⊢ 𝐴 ∈ V
3		elabf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4		nfcv	⊢ Ⅎ 𝑥 𝐴
5	4 1 3	elabgf	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 ) )
6	2 5	ax-mp	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )