Theorem nfrelp

Description: Bound-variable hypothesis builder for a relation-preserving function. (Contributed by Eric Schmidt, 11-Oct-2025)

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

Proof

Step	Hyp	Ref	Expression
1		nfrelp.1	|- F/_ x H
2		nfrelp.2	|- F/_ x R
3		nfrelp.3	|- F/_ x S
4		nfrelp.4	|- F/_ x A
5		nfrelp.5	|- F/_ x B
6		df-relp	|- ( H RelPres R , S ( A , B ) <-> ( H : A --> B /\ A. y e. A A. z e. A ( y R z -> ( H ` y ) S ( H ` z ) ) ) )
7	1 4 5	nff	|- F/ x H : A --> 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	nfim	|- 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 --> B /\ A. y e. A A. z e. A ( y R z -> ( H ` y ) S ( H ` z ) ) )
18	6 17	nfxfr	|- F/ x H RelPres R , S ( A , B )