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

Metamath Proof Explorer

Theorem nfbrd

Description: Deduction version of bound-variable hypothesis builder nfbr . (Contributed by NM, 13-Dec-2005) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypotheses nfbrd.2 ⊢ φ → Ⅎ _ x A
nfbrd.3 ⊢ φ → Ⅎ _ x R
nfbrd.4 ⊢ φ → Ⅎ _ x B
Assertion nfbrd ⊢ φ → Ⅎ x A R B

Proof

Step Hyp Ref Expression
1 nfbrd.2 ⊢ φ → Ⅎ _ x A
2 nfbrd.3 ⊢ φ → Ⅎ _ x R
3 nfbrd.4 ⊢ φ → Ⅎ _ x B
4 df-br ⊢ A R B ↔ A B ∈ R
5 1 3 nfopd ⊢ φ → Ⅎ _ x A B
6 5 2 nfeld ⊢ φ → Ⅎ x A B ∈ R
7 4 6 nfxfrd ⊢ φ → Ⅎ x A R B