Metamath Proof Explorer

Theorem prtlem5

Description: Lemma for prter1 , prter2 , prter3 and prtex . (Contributed by Rodolfo Medina, 25-Sep-2010) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion prtlem5 
|- ( [ s / v ] [ r / u ] E. x e. A ( u e. x /\ v e. x ) <-> E. x e. A ( r e. x /\ s e. x ) )

Proof

Step Hyp Ref Expression
1 elequ1 
 |-  ( u = r -> ( u e. x <-> r e. x ) )
2 elequ1 
 |-  ( v = s -> ( v e. x <-> s e. x ) )
3 1 2 bi2anan9r 
 |-  ( ( v = s /\ u = r ) -> ( ( u e. x /\ v e. x ) <-> ( r e. x /\ s e. x ) ) )
4 3 rexbidv 
 |-  ( ( v = s /\ u = r ) -> ( E. x e. A ( u e. x /\ v e. x ) <-> E. x e. A ( r e. x /\ s e. x ) ) )
5 4 2sbievw 
 |-  ( [ s / v ] [ r / u ] E. x e. A ( u e. x /\ v e. x ) <-> E. x e. A ( r e. x /\ s e. x ) )