Theorem bnj90

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj90.1	|- Y e. _V
Assertion	bnj90	|- ( [. Y / x ]. z Fn x <-> z Fn Y )

Proof

Step	Hyp	Ref	Expression
1		bnj90.1	|- Y e. _V
2		fneq2	|- ( x = y -> ( z Fn x <-> z Fn y ) )
3		fneq2	|- ( y = Y -> ( z Fn y <-> z Fn Y ) )
4	2 3	sbcie2g	|- ( Y e. _V -> ( [. Y / x ]. z Fn x <-> z Fn Y ) )
5	1 4	ax-mp	|- ( [. Y / x ]. z Fn x <-> z Fn Y )