Theorem brtxpsd

Description: Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brtxpsd.1	|- A e. _V
	brtxpsd.2	|- B e. _V
Assertion	brtxpsd	|- ( -. A ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) B <-> A. x ( x e. B <-> x R A ) )

Proof

Step	Hyp	Ref	Expression
1		brtxpsd.1	|- A e. _V
2		brtxpsd.2	|- B e. _V
3		df-br	|- ( A ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) B <-> <. A , B >. e. ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) )
4		opex	|- <. A , B >. e. _V
5	4	elrn	|- ( <. A , B >. e. ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) <-> E. x x ( ( _V (x) _E ) /_\ ( R (x) _V ) ) <. A , B >. )
6		brsymdif	|- ( x ( ( _V (x) _E ) /_\ ( R (x) _V ) ) <. A , B >. <-> -. ( x ( _V (x) _E ) <. A , B >. <-> x ( R (x) _V ) <. A , B >. ) )
7		brv	|- x _V A
8		vex	|- x e. _V
9	8 1 2	brtxp	|- ( x ( _V (x) _E ) <. A , B >. <-> ( x _V A /\ x _E B ) )
10	7 9	mpbiran	|- ( x ( _V (x) _E ) <. A , B >. <-> x _E B )
11	2	epeli	|- ( x _E B <-> x e. B )
12	10 11	bitri	|- ( x ( _V (x) _E ) <. A , B >. <-> x e. B )
13		brv	|- x _V B
14	8 1 2	brtxp	|- ( x ( R (x) _V ) <. A , B >. <-> ( x R A /\ x _V B ) )
15	13 14	mpbiran2	|- ( x ( R (x) _V ) <. A , B >. <-> x R A )
16	12 15	bibi12i	|- ( ( x ( _V (x) _E ) <. A , B >. <-> x ( R (x) _V ) <. A , B >. ) <-> ( x e. B <-> x R A ) )
17	6 16	xchbinx	|- ( x ( ( _V (x) _E ) /_\ ( R (x) _V ) ) <. A , B >. <-> -. ( x e. B <-> x R A ) )
18	17	exbii	|- ( E. x x ( ( _V (x) _E ) /_\ ( R (x) _V ) ) <. A , B >. <-> E. x -. ( x e. B <-> x R A ) )
19	5 18	bitri	|- ( <. A , B >. e. ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) <-> E. x -. ( x e. B <-> x R A ) )
20		exnal	|- ( E. x -. ( x e. B <-> x R A ) <-> -. A. x ( x e. B <-> x R A ) )
21	3 19 20	3bitrri	|- ( -. A. x ( x e. B <-> x R A ) <-> A ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) B )
22	21	con1bii	|- ( -. A ran ( ( _V (x) _E ) /_\ ( R (x) _V ) ) B <-> A. x ( x e. B <-> x R A ) )