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

Metamath Proof Explorer

Theorem csbie2t

Description: Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 ). (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses csbie2t.1 
|- A e. _V
csbie2t.2 
|- B e. _V
Assertion csbie2t 
|- ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> [_ A / x ]_ [_ B / y ]_ C = D )

Proof

Step Hyp Ref Expression
1 csbie2t.1 
 |-  A e. _V
2 csbie2t.2 
 |-  B e. _V
3 nfa1 
 |-  F/ x A. x A. y ( ( x = A /\ y = B ) -> C = D )
4 nfcvd 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> F/_ x D )
5 1 a1i 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> A e. _V )
6 nfa2 
 |-  F/ y A. x A. y ( ( x = A /\ y = B ) -> C = D )
7 nfv 
 |-  F/ y x = A
8 6 7 nfan 
 |-  F/ y ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) /\ x = A )
9 nfcvd 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) /\ x = A ) -> F/_ y D )
10 2 a1i 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) /\ x = A ) -> B e. _V )
11 2sp 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> ( ( x = A /\ y = B ) -> C = D ) )
12 11 impl 
 |-  ( ( ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) /\ x = A ) /\ y = B ) -> C = D )
13 8 9 10 12 csbiedf 
 |-  ( ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) /\ x = A ) -> [_ B / y ]_ C = D )
14 3 4 5 13 csbiedf 
 |-  ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> [_ A / x ]_ [_ B / y ]_ C = D )