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		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall yℲxy\in A$$
6	1 5	sylib	$$⊢\phi \to \forall yℲxy\in A$$
7	6	19.21bi	$$⊢\phi \to Ⅎxy\in A$$
8		df-nfc	$$⊢\underset{\_}{Ⅎ}xB\leftrightarrow \forall yℲxy\in B$$
9	2 8	sylib	$$⊢\phi \to \forall yℲxy\in B$$
10	9	19.21bi	$$⊢\phi \to Ⅎxy\in B$$
11	7 10	nfbid	$$⊢\phi \to Ⅎx\left(y\in A\leftrightarrow y\in B\right)$$
12	4 11	nfald	$$⊢\phi \to Ⅎx\forall y\left(y\in A\leftrightarrow y\in B\right)$$
13	3 12	nfxfrd	$$⊢\phi \to ℲxA=B$$