Theorem nfeqd

Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016)

	Ref	Expression
Hypotheses	nfeqd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfeqd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfeqd	$$⊢\phi \to ℲxA=B$$

Proof

Step	Hyp	Ref	Expression
1		nfeqd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfeqd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
3		dfcleq	$$⊢A=B\leftrightarrow \forall y\left(y\in A\leftrightarrow y\in B\right)$$
4		nfv	$$⊢Ⅎy\phi$$
5	1	nfcrd	$$⊢\phi \to Ⅎxy\in A$$
6	2	nfcrd	$$⊢\phi \to Ⅎxy\in B$$
7	5 6	nfbid	$$⊢\phi \to Ⅎx\left(y\in A\leftrightarrow y\in B\right)$$
8	4 7	nfald	$$⊢\phi \to Ⅎx\forall y\left(y\in A\leftrightarrow y\in B\right)$$
9	3 8	nfxfrd	$$⊢\phi \to ℲxA=B$$