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

Metamath Proof Explorer

Theorem sbc2iegf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses sbc2iegf.1 
|- F/ x ps
sbc2iegf.2 
|- F/ y ps
sbc2iegf.3 
|- F/ x B e. W
sbc2iegf.4 
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
Assertion sbc2iegf 
|- ( ( A e. V /\ B e. W ) -> ( [. A / x ]. [. B / y ]. ph <-> ps ) )

Proof

Step Hyp Ref Expression
1 sbc2iegf.1 
 |-  F/ x ps
2 sbc2iegf.2 
 |-  F/ y ps
3 sbc2iegf.3 
 |-  F/ x B e. W
4 sbc2iegf.4 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
5 simpl 
 |-  ( ( A e. V /\ B e. W ) -> A e. V )
6 simpl 
 |-  ( ( B e. W /\ x = A ) -> B e. W )
7 4 adantll 
 |-  ( ( ( B e. W /\ x = A ) /\ y = B ) -> ( ph <-> ps ) )
8 nfv 
 |-  F/ y ( B e. W /\ x = A )
9 2 a1i 
 |-  ( ( B e. W /\ x = A ) -> F/ y ps )
10 6 7 8 9 sbciedf 
 |-  ( ( B e. W /\ x = A ) -> ( [. B / y ]. ph <-> ps ) )
11 10 adantll 
 |-  ( ( ( A e. V /\ B e. W ) /\ x = A ) -> ( [. B / y ]. ph <-> ps ) )
12 nfv 
 |-  F/ x A e. V
13 12 3 nfan 
 |-  F/ x ( A e. V /\ B e. W )
14 1 a1i 
 |-  ( ( A e. V /\ B e. W ) -> F/ x ps )
15 5 11 13 14 sbciedf 
 |-  ( ( A e. V /\ B e. W ) -> ( [. A / x ]. [. B / y ]. ph <-> ps ) )