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

Metamath Proof Explorer

Theorem nfop

Description: Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995)

Ref Expression
Hypotheses nfop.1 ⊢ Ⅎ _ x A
nfop.2 ⊢ Ⅎ _ x B
Assertion nfop ⊢ Ⅎ _ x A B

Proof

Step Hyp Ref Expression
1 nfop.1 ⊢ Ⅎ _ x A
2 nfop.2 ⊢ Ⅎ _ x B
3 dfopif ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅
4 1 nfel1 ⊢ Ⅎ x A ∈ V
5 2 nfel1 ⊢ Ⅎ x B ∈ V
6 4 5 nfan ⊢ Ⅎ x A ∈ V ∧ B ∈ V
7 1 nfsn ⊢ Ⅎ _ x A
8 1 2 nfpr ⊢ Ⅎ _ x A B
9 7 8 nfpr ⊢ Ⅎ _ x A A B
10 nfcv ⊢ Ⅎ _ x ∅
11 6 9 10 nfif ⊢ Ⅎ _ x if A ∈ V ∧ B ∈ V A A B ∅
12 3 11 nfcxfr ⊢ Ⅎ _ x A B