Theorem nffr

Description: Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nffr.r	⊢ Ⅎ 𝑥 𝑅
	nffr.a	⊢ Ⅎ 𝑥 𝐴
Assertion	nffr	⊢ Ⅎ 𝑥 𝑅 Fr 𝐴

Proof

Step	Hyp	Ref	Expression
1		nffr.r	⊢ Ⅎ 𝑥 𝑅
2		nffr.a	⊢ Ⅎ 𝑥 𝐴
3		df-fr	⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏 ) )
4		nfcv	⊢ Ⅎ 𝑥 𝑎
5	4 2	nfss	⊢ Ⅎ 𝑥 𝑎 ⊆ 𝐴
6		nfv	⊢ Ⅎ 𝑥 𝑎 ≠ ∅
7	5 6	nfan	⊢ Ⅎ 𝑥 ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ )
8		nfcv	⊢ Ⅎ 𝑥 𝑐
9		nfcv	⊢ Ⅎ 𝑥 𝑏
10	8 1 9	nfbr	⊢ Ⅎ 𝑥 𝑐 𝑅 𝑏
11	10	nfn	⊢ Ⅎ 𝑥 ¬ 𝑐 𝑅 𝑏
12	4 11	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏
13	4 12	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏
14	7 13	nfim	⊢ Ⅎ 𝑥 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏 )
15	14	nfal	⊢ Ⅎ 𝑥 ∀ 𝑎 ( ( 𝑎 ⊆ 𝐴 ∧ 𝑎 ≠ ∅ ) → ∃ 𝑏 ∈ 𝑎 ∀ 𝑐 ∈ 𝑎 ¬ 𝑐 𝑅 𝑏 )
16	3 15	nfxfr	⊢ Ⅎ 𝑥 𝑅 Fr 𝐴