This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfpred

Description: Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018)

Ref Expression
Hypotheses nfpred.1 ⊢ Ⅎ _ x R
nfpred.2 ⊢ Ⅎ _ x A
nfpred.3 ⊢ Ⅎ _ x X
Assertion nfpred ⊢ Ⅎ _ x Pred R A X

Proof

Step Hyp Ref Expression
1 nfpred.1 ⊢ Ⅎ _ x R
2 nfpred.2 ⊢ Ⅎ _ x A
3 nfpred.3 ⊢ Ⅎ _ x X
4 df-pred ⊢ Pred R A X = A ∩ R -1 X
5 1 nfcnv ⊢ Ⅎ _ x R -1
6 3 nfsn ⊢ Ⅎ _ x X
7 5 6 nfima ⊢ Ⅎ _ x R -1 X
8 2 7 nfin ⊢ Ⅎ _ x A ∩ R -1 X
9 4 8 nfcxfr ⊢ Ⅎ _ x Pred R A X