Theorem nfriotad

Description: Deduction version of nfriota . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfriotadw when possible. (Contributed by NM, 18-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfriotad.1	|- F/ y ph
	nfriotad.2	|- ( ph -> F/ x ps )
	nfriotad.3	|- ( ph -> F/_ x A )
Assertion	nfriotad	|- ( ph -> F/_ x ( iota_ y e. A ps ) )

Proof

Step	Hyp	Ref	Expression
1		nfriotad.1	|- F/ y ph
2		nfriotad.2	|- ( ph -> F/ x ps )
3		nfriotad.3	|- ( ph -> F/_ x A )
4		df-riota	|- ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) )
5		nfnae	|- F/ y -. A. x x = y
6	1 5	nfan	|- F/ y ( ph /\ -. A. x x = y )
7		nfcvf	|- ( -. A. x x = y -> F/_ x y )
8	7	adantl	|- ( ( ph /\ -. A. x x = y ) -> F/_ x y )
9	3	adantr	|- ( ( ph /\ -. A. x x = y ) -> F/_ x A )
10	8 9	nfeld	|- ( ( ph /\ -. A. x x = y ) -> F/ x y e. A )
11	2	adantr	|- ( ( ph /\ -. A. x x = y ) -> F/ x ps )
12	10 11	nfand	|- ( ( ph /\ -. A. x x = y ) -> F/ x ( y e. A /\ ps ) )
13	6 12	nfiotad	|- ( ( ph /\ -. A. x x = y ) -> F/_ x ( iota y ( y e. A /\ ps ) ) )
14	13	ex	|- ( ph -> ( -. A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) ) )
15		nfiota1	|- F/_ y ( iota y ( y e. A /\ ps ) )
16		eqidd	|- ( A. x x = y -> ( iota y ( y e. A /\ ps ) ) = ( iota y ( y e. A /\ ps ) ) )
17	16	drnfc1	|- ( A. x x = y -> ( F/_ x ( iota y ( y e. A /\ ps ) ) <-> F/_ y ( iota y ( y e. A /\ ps ) ) ) )
18	15 17	mpbiri	|- ( A. x x = y -> F/_ x ( iota y ( y e. A /\ ps ) ) )
19	14 18	pm2.61d2	|- ( ph -> F/_ x ( iota y ( y e. A /\ ps ) ) )
20	4 19	nfcxfrd	|- ( ph -> F/_ x ( iota_ y e. A ps ) )