Theorem nfrelp

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

	Ref	Expression
Hypotheses	nfrelp.1	⊢ Ⅎ 𝑥 𝐻
	nfrelp.2	⊢ Ⅎ 𝑥 𝑅
	nfrelp.3	⊢ Ⅎ 𝑥 𝑆
	nfrelp.4	⊢ Ⅎ 𝑥 𝐴
	nfrelp.5	⊢ Ⅎ 𝑥 𝐵
Assertion	nfrelp	⊢ Ⅎ 𝑥 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfrelp.1	⊢ Ⅎ 𝑥 𝐻
2		nfrelp.2	⊢ Ⅎ 𝑥 𝑅
3		nfrelp.3	⊢ Ⅎ 𝑥 𝑆
4		nfrelp.4	⊢ Ⅎ 𝑥 𝐴
5		nfrelp.5	⊢ Ⅎ 𝑥 𝐵
6		df-relp	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) ) ) )
7	1 4 5	nff	⊢ Ⅎ 𝑥 𝐻 : 𝐴 ⟶ 𝐵
8		nfcv	⊢ Ⅎ 𝑥 𝑦
9		nfcv	⊢ Ⅎ 𝑥 𝑧
10	8 2 9	nfbr	⊢ Ⅎ 𝑥 𝑦 𝑅 𝑧
11	1 8	nffv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑦 )
12	1 9	nffv	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑧 )
13	11 3 12	nfbr	⊢ Ⅎ 𝑥 ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 )
14	10 13	nfim	⊢ Ⅎ 𝑥 ( 𝑦 𝑅 𝑧 → ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) )
15	4 14	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) )
16	4 15	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) )
17	7 16	nfan	⊢ Ⅎ 𝑥 ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → ( 𝐻 ‘ 𝑦 ) 𝑆 ( 𝐻 ‘ 𝑧 ) ) )
18	6 17	nfxfr	⊢ Ⅎ 𝑥 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 )