Metamath Proof Explorer


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 _ x B
Assertion bj-seex R Se A B A x A | x R B V

Proof

Step Hyp Ref Expression
1 bj-seex.nf _ x B
2 df-se R Se A y A x A | x R y V
3 1 nfeq2 x y = B
4 breq2 y = B x R y x R B
5 3 4 rabbid y = B x A | x R y = x A | x R B
6 5 eleq1d y = B x A | x R y V x A | x R B V
7 6 rspccva y A x A | x R y V B A x A | x R B V
8 2 7 sylanb R Se A B A x A | x R B V