Metamath Proof Explorer


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 | u A x u y u
Assertion prtlem19 Prt A v A z v v = z ˙

Proof

Step Hyp Ref Expression
1 prtlem18.1 ˙ = x y | u A x u y u
2 1 prtlem18 Prt A v A z v w v z ˙ w
3 2 imp Prt A v A z v w v z ˙ w
4 vex w V
5 vex z V
6 4 5 elec w z ˙ z ˙ w
7 3 6 bitr4di Prt A v A z v w v w z ˙
8 7 eqrdv Prt A v A z v v = z ˙
9 8 ex Prt A v A z v v = z ˙