Theorem bnj23

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	bnj23.1	|- B = { x e. A | -. ph }
Assertion	bnj23	|- ( A. z e. B -. z R y -> A. w e. A ( w R y -> [. w / x ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		bnj23.1	|- B = { x e. A | -. ph }
2		sbcng	|- ( w e. _V -> ( [. w / x ]. -. ph <-> -. [. w / x ]. ph ) )
3	2	elv	|- ( [. w / x ]. -. ph <-> -. [. w / x ]. ph )
4	1	eleq2i	|- ( w e. B <-> w e. { x e. A | -. ph } )
5		nfcv	|- F/_ x A
6	5	elrabsf	|- ( w e. { x e. A | -. ph } <-> ( w e. A /\ [. w / x ]. -. ph ) )
7	4 6	bitri	|- ( w e. B <-> ( w e. A /\ [. w / x ]. -. ph ) )
8		breq1	|- ( z = w -> ( z R y <-> w R y ) )
9	8	notbid	|- ( z = w -> ( -. z R y <-> -. w R y ) )
10	9	rspccv	|- ( A. z e. B -. z R y -> ( w e. B -> -. w R y ) )
11	7 10	syl5bir	|- ( A. z e. B -. z R y -> ( ( w e. A /\ [. w / x ]. -. ph ) -> -. w R y ) )
12	11	expdimp	|- ( ( A. z e. B -. z R y /\ w e. A ) -> ( [. w / x ]. -. ph -> -. w R y ) )
13	3 12	syl5bir	|- ( ( A. z e. B -. z R y /\ w e. A ) -> ( -. [. w / x ]. ph -> -. w R y ) )
14	13	con4d	|- ( ( A. z e. B -. z R y /\ w e. A ) -> ( w R y -> [. w / x ]. ph ) )
15	14	ralrimiva	|- ( A. z e. B -. z R y -> A. w e. A ( w R y -> [. w / x ]. ph ) )