Theorem nfrelp

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

	Ref	Expression
Hypotheses	nfrelp.1	$$⊢\underset{\_}{Ⅎ}xH$$
	nfrelp.2	$$⊢\underset{\_}{Ⅎ}xR$$
	nfrelp.3	$$⊢\underset{\_}{Ⅎ}xS$$
	nfrelp.4	$$⊢\underset{\_}{Ⅎ}xA$$
	nfrelp.5	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfrelp	Could not format assertion : No typesetting found for |- F/ x H RelPres R , S ( A , B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nfrelp.1	$$⊢\underset{\_}{Ⅎ}xH$$
2		nfrelp.2	$$⊢\underset{\_}{Ⅎ}xR$$
3		nfrelp.3	$$⊢\underset{\_}{Ⅎ}xS$$
4		nfrelp.4	$$⊢\underset{\_}{Ⅎ}xA$$
5		nfrelp.5	$$⊢\underset{\_}{Ⅎ}xB$$
6		df-relp	Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
7	1 4 5	nff	$$⊢ℲxH:A⟶B$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
10	8 2 9	nfbr	$$⊢ℲxyRz$$
11	1 8	nffv	$$⊢\underset{\_}{Ⅎ}xH\left(y\right)$$
12	1 9	nffv	$$⊢\underset{\_}{Ⅎ}xH\left(z\right)$$
13	11 3 12	nfbr	$$⊢ℲxH\left(y\right)SH\left(z\right)$$
14	10 13	nfim	$$⊢Ⅎx\left(yRz\to H\left(y\right)SH\left(z\right)\right)$$
15	4 14	nfralw	$$⊢Ⅎx\forall z\in A\left(yRz\to H\left(y\right)SH\left(z\right)\right)$$
16	4 15	nfralw	$$⊢Ⅎx\forall y\in A\forall z\in A\left(yRz\to H\left(y\right)SH\left(z\right)\right)$$
17	7 16	nfan	$$⊢Ⅎx\left(H:A⟶B\wedge \forall y\in A\forall z\in A\left(yRz\to H\left(y\right)SH\left(z\right)\right)\right)$$
18	6 17	nfxfr	Could not format F/ x H RelPres R , S ( A , B ) : No typesetting found for |- F/ x H RelPres R , S ( A , B ) with typecode |-