Theorem drnfc2

Description: Formula-building lemma for use with the Distinctor Reduction Theorem. Proof revision is marked as discouraged because the minimizer replaces albidv with dral2 , leading to a one byte longer proof. However feel free to manually edit it according to conventions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	drnfc1.1	|- ( A. x x = y -> A = B )
Assertion	drnfc2	|- ( A. x x = y -> ( F/_ z A <-> F/_ z B ) )

Proof

Step	Hyp	Ref	Expression
1		drnfc1.1	|- ( A. x x = y -> A = B )
2	1	eleq2d	|- ( A. x x = y -> ( w e. A <-> w e. B ) )
3	2	drnf2	|- ( A. x x = y -> ( F/ z w e. A <-> F/ z w e. B ) )
4	3	albidv	|- ( A. x x = y -> ( A. w F/ z w e. A <-> A. w F/ z w e. B ) )
5		df-nfc	|- ( F/_ z A <-> A. w F/ z w e. A )
6		df-nfc	|- ( F/_ z B <-> A. w F/ z w e. B )
7	4 5 6	3bitr4g	|- ( A. x x = y -> ( F/_ z A <-> F/_ z B ) )