Metamath Proof Explorer


Theorem nfrelp

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

Ref Expression
Hypotheses nfrelp.1 _ x H
nfrelp.2 _ x R
nfrelp.3 _ x S
nfrelp.4 _ x A
nfrelp.5 _ x B
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 _ x H
2 nfrelp.2 _ x R
3 nfrelp.3 _ x S
4 nfrelp.4 _ x A
5 nfrelp.5 _ x B
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 x H : A B
8 nfcv _ x y
9 nfcv _ x z
10 8 2 9 nfbr x y R z
11 1 8 nffv _ x H y
12 1 9 nffv _ x H z
13 11 3 12 nfbr x H y S H z
14 10 13 nfim x y R z H y S H z
15 4 14 nfralw x z A y R z H y S H z
16 4 15 nfralw x y A z A y R z H y S H z
17 7 16 nfan x H : A B y A z A y R z H y S H z
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 |-