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

Metamath Proof Explorer

Theorem spc2d

Description: Specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Hypotheses spc2ed.x 
|- F/ x ch
spc2ed.y 
|- F/ y ch
spc2ed.1 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion spc2d 
|- ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( A. x A. y ps -> ch ) )

Proof

Step Hyp Ref Expression
1 spc2ed.x 
 |-  F/ x ch
2 spc2ed.y 
 |-  F/ y ch
3 spc2ed.1 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
4 2nalexn 
 |-  ( -. A. x A. y ps <-> E. x E. y -. ps )
5 4 con1bii 
 |-  ( -. E. x E. y -. ps <-> A. x A. y ps )
6 1 nfn 
 |-  F/ x -. ch
7 2 nfn 
 |-  F/ y -. ch
8 3 notbid 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( -. ps <-> -. ch ) )
9 6 7 8 spc2ed 
 |-  ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( -. ch -> E. x E. y -. ps ) )
10 9 con1d 
 |-  ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( -. E. x E. y -. ps -> ch ) )
11 5 10 biimtrrid 
 |-  ( ( ph /\ ( A e. V /\ B e. W ) ) -> ( A. x A. y ps -> ch ) )