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 ) )

Metamath Proof Explorer

Theorem brtxpsd

Proof