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

Metamath Proof Explorer

Theorem eqabf

Description: Equality of a class variable and a class abstraction. In this version, the fact that x is a nonfree variable in A is explicitly stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017) Avoid ax-13 . (Revised by Wolf Lammen, 13-May-2023)

		Ref	Expression
	Hypothesis	eqabf.0	\|- F/_ x A
	Assertion	eqabf	\|- ( A = { x \| ph } <-> A. x ( x e. A <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		eqabf.0	\|- F/_ x A
2		nfab1	\|- F/_ x { x \| ph }
3	1 2	cleqf	\|- ( A = { x \| ph } <-> A. x ( x e. A <-> x e. { x \| ph } ) )
4		abid	\|- ( x e. { x \| ph } <-> ph )
5	4	bibi2i	\|- ( ( x e. A <-> x e. { x \| ph } ) <-> ( x e. A <-> ph ) )
6	5	albii	\|- ( A. x ( x e. A <-> x e. { x \| ph } ) <-> A. x ( x e. A <-> ph ) )
7	3 6	bitri	\|- ( A = { x \| ph } <-> A. x ( x e. A <-> ph ) )