Theorem bj-seex

Description: Version of seex with a disjoint variable condition replaced by a nonfreeness hypothesis (for the sake of illustration). (Contributed by BJ, 27-Apr-2019)

	Ref	Expression
Hypothesis	bj-seex.nf	⊢ Ⅎ 𝑥 𝐵
Assertion	bj-seex	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		bj-seex.nf	⊢ Ⅎ 𝑥 𝐵
2		df-se	⊢ ( 𝑅 Se 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V )
3	1	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐵
4		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝐵 ) )
5	3 4	rabbid	⊢ ( 𝑦 = 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } = { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } )
6	5	eleq1d	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ↔ { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V ) )
7	6	rspccva	⊢ ( ( ∀ 𝑦 ∈ 𝐴 { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝑦 } ∈ V ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V )
8	2 7	sylanb	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 𝑅 𝐵 } ∈ V )