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

Metamath Proof Explorer

Theorem nfse

Description: Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015) (Revised by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypotheses nffr.r ⊢ Ⅎ _ x R
nffr.a ⊢ Ⅎ _ x A
Assertion nfse ⊢ Ⅎ x R Se A

Proof

Step Hyp Ref Expression
1 nffr.r ⊢ Ⅎ _ x R
2 nffr.a ⊢ Ⅎ _ x A
3 df-se ⊢ R Se A ↔ ∀ b ∈ A a ∈ A | a R b ∈ V
4 nfcv ⊢ Ⅎ _ x a
5 nfcv ⊢ Ⅎ _ x b
6 4 1 5 nfbr ⊢ Ⅎ x a R b
7 6 2 nfrabw ⊢ Ⅎ _ x a ∈ A | a R b
8 7 nfel1 ⊢ Ⅎ x a ∈ A | a R b ∈ V
9 2 8 nfralw ⊢ Ⅎ x ∀ b ∈ A a ∈ A | a R b ∈ V
10 3 9 nfxfr ⊢ Ⅎ x R Se A