Theorem brtxpsd3

Description: A third common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 3-May-2014)

	Ref	Expression
Hypotheses	brtxpsd2.1	|- A e. _V
	brtxpsd2.2	|- B e. _V
	brtxpsd2.3	|- R = ( C \ ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) )
	brtxpsd2.4	|- A C B
	brtxpsd3.5	|- ( x e. X <-> x S A )
Assertion	brtxpsd3	|- ( A R B <-> B = X )

Proof

Step	Hyp	Ref	Expression
1		brtxpsd2.1	|- A e. _V
2		brtxpsd2.2	|- B e. _V
3		brtxpsd2.3	|- R = ( C \ ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) )
4		brtxpsd2.4	|- A C B
5		brtxpsd3.5	|- ( x e. X <-> x S A )
6	5	bibi2i	|- ( ( x e. B <-> x e. X ) <-> ( x e. B <-> x S A ) )
7	6	albii	|- ( A. x ( x e. B <-> x e. X ) <-> A. x ( x e. B <-> x S A ) )
8		dfcleq	|- ( B = X <-> A. x ( x e. B <-> x e. X ) )
9	1 2 3 4	brtxpsd2	|- ( A R B <-> A. x ( x e. B <-> x S A ) )
10	7 8 9	3bitr4ri	|- ( A R B <-> B = X )