Theorem brtxpsd2

Description: Another common abbreviation for quantifier-free definitions. (Contributed by Scott Fenton, 21-Apr-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
Assertion	brtxpsd2	|- ( A R B <-> A. x ( x e. B <-> x S A ) )

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	3	breqi	|- ( A R B <-> A ( C \ ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) ) B )
6		brdif	|- ( A ( C \ ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) ) B <-> ( A C B /\ -. A ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) B ) )
7	5 6	bitri	|- ( A R B <-> ( A C B /\ -. A ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) B ) )
8	4 7	mpbiran	|- ( A R B <-> -. A ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) B )
9	1 2	brtxpsd	|- ( -. A ran ( ( _V (x) _E ) /_\ ( S (x) _V ) ) B <-> A. x ( x e. B <-> x S A ) )
10	8 9	bitri	|- ( A R B <-> A. x ( x e. B <-> x S A ) )