This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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