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	⊢ Ⅎ 𝑥 𝑅
	nffr.a	⊢ Ⅎ 𝑥 𝐴
Assertion	nfse	⊢ Ⅎ 𝑥 𝑅 Se 𝐴

Proof

Step	Hyp	Ref	Expression
1		nffr.r	⊢ Ⅎ 𝑥 𝑅
2		nffr.a	⊢ Ⅎ 𝑥 𝐴
3		df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑏 ∈ 𝐴 { 𝑎 ∈ 𝐴 ∣ 𝑎 𝑅 𝑏 } ∈ V )
4		nfcv	⊢ Ⅎ 𝑥 𝑎
5		nfcv	⊢ Ⅎ 𝑥 𝑏
6	4 1 5	nfbr	⊢ Ⅎ 𝑥 𝑎 𝑅 𝑏
7	6 2	nfrabw	⊢ Ⅎ 𝑥 { 𝑎 ∈ 𝐴 ∣ 𝑎 𝑅 𝑏 }
8	7	nfel1	⊢ Ⅎ 𝑥 { 𝑎 ∈ 𝐴 ∣ 𝑎 𝑅 𝑏 } ∈ V
9	2 8	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑏 ∈ 𝐴 { 𝑎 ∈ 𝐴 ∣ 𝑎 𝑅 𝑏 } ∈ V
10	3 9	nfxfr	⊢ Ⅎ 𝑥 𝑅 Se 𝐴