Theorem prtlem19

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	prtlem18.1	|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
Assertion	prtlem19	|- ( Prt A -> ( ( v e. A /\ z e. v ) -> v = [ z ] .~ ) )

Proof

Step	Hyp	Ref	Expression
1		prtlem18.1	|- .~ = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) }
2	1	prtlem18	|- ( Prt A -> ( ( v e. A /\ z e. v ) -> ( w e. v <-> z .~ w ) ) )
3	2	imp	|- ( ( Prt A /\ ( v e. A /\ z e. v ) ) -> ( w e. v <-> z .~ w ) )
4		vex	|- w e. _V
5		vex	|- z e. _V
6	4 5	elec	|- ( w e. [ z ] .~ <-> z .~ w )
7	3 6	bitr4di	|- ( ( Prt A /\ ( v e. A /\ z e. v ) ) -> ( w e. v <-> w e. [ z ] .~ ) )
8	7	eqrdv	|- ( ( Prt A /\ ( v e. A /\ z e. v ) ) -> v = [ z ] .~ )
9	8	ex	|- ( Prt A -> ( ( v e. A /\ z e. v ) -> v = [ z ] .~ ) )