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

Metamath Proof Explorer

Theorem nfwe

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

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

Proof

Step	Hyp	Ref	Expression
1		nffr.r	⊢ Ⅎ 𝑥 𝑅
2		nffr.a	⊢ Ⅎ 𝑥 𝐴
3		df-we	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )
4	1 2	nffr	⊢ Ⅎ 𝑥 𝑅 Fr 𝐴
5	1 2	nfso	⊢ Ⅎ 𝑥 𝑅 Or 𝐴
6	4 5	nfan	⊢ Ⅎ 𝑥 ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 )
7	3 6	nfxfr	⊢ Ⅎ 𝑥 𝑅 We 𝐴