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 ⊢ Ⅎ _ x R
nffr.a ⊢ Ⅎ _ x A
Assertion nfwe ⊢ Ⅎ x R We A

Proof

Step Hyp Ref Expression
1 nffr.r ⊢ Ⅎ _ x R
2 nffr.a ⊢ Ⅎ _ x A
3 df-we ⊢ R We A ↔ R Fr A ∧ R Or A
4 1 2 nffr ⊢ Ⅎ x R Fr A
5 1 2 nfso ⊢ Ⅎ x R Or A
6 4 5 nfan ⊢ Ⅎ x R Fr A ∧ R Or A
7 3 6 nfxfr ⊢ Ⅎ x R We A