Theorem nfiso

Description: Bound-variable hypothesis builder for an isomorphism. (Contributed by NM, 17-May-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Hypotheses	nfiso.1	|- F/_ x H
	nfiso.2	|- F/_ x R
	nfiso.3	|- F/_ x S
	nfiso.4	|- F/_ x A
	nfiso.5	|- F/_ x B
Assertion	nfiso	|- F/ x H Isom R , S ( A , B )

Proof

Step	Hyp	Ref	Expression
1		nfiso.1	|- F/_ x H
2		nfiso.2	|- F/_ x R
3		nfiso.3	|- F/_ x S
4		nfiso.4	|- F/_ x A
5		nfiso.5	|- F/_ x B
6		df-isom	|- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. y e. A A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) ) ) )
7	1 4 5	nff1o	|- F/ x H : A -1-1-onto-> B
8		nfcv	|- F/_ x y
9		nfcv	|- F/_ x z
10	8 2 9	nfbr	|- F/ x y R z
11	1 8	nffv	|- F/_ x ( H ` y )
12	1 9	nffv	|- F/_ x ( H ` z )
13	11 3 12	nfbr	|- F/ x ( H ` y ) S ( H ` z )
14	10 13	nfbi	|- F/ x ( y R z <-> ( H ` y ) S ( H ` z ) )
15	4 14	nfralw	|- F/ x A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) )
16	4 15	nfralw	|- F/ x A. y e. A A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) )
17	7 16	nfan	|- F/ x ( H : A -1-1-onto-> B /\ A. y e. A A. z e. A ( y R z <-> ( H ` y ) S ( H ` z ) ) )
18	6 17	nfxfr	|- F/ x H Isom R , S ( A , B )