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

Metamath Proof Explorer

Theorem csbiebg

Description: Bidirectional conversion between an implicit class substitution hypothesis x = A -> B = C and its explicit substitution equivalent. (Contributed by NM, 24-Mar-2013) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypothesis csbiebg.2 
|- F/_ x C
Assertion csbiebg 
|- ( A e. V -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )

Proof

Step Hyp Ref Expression
1 csbiebg.2 
 |-  F/_ x C
2 eqeq2 
 |-  ( a = A -> ( x = a <-> x = A ) )
3 2 imbi1d 
 |-  ( a = A -> ( ( x = a -> B = C ) <-> ( x = A -> B = C ) ) )
4 3 albidv 
 |-  ( a = A -> ( A. x ( x = a -> B = C ) <-> A. x ( x = A -> B = C ) ) )
5 csbeq1 
 |-  ( a = A -> [_ a / x ]_ B = [_ A / x ]_ B )
6 5 eqeq1d 
 |-  ( a = A -> ( [_ a / x ]_ B = C <-> [_ A / x ]_ B = C ) )
7 vex 
 |-  a e. _V
8 7 1 csbieb 
 |-  ( A. x ( x = a -> B = C ) <-> [_ a / x ]_ B = C )
9 4 6 8 vtoclbg 
 |-  ( A e. V -> ( A. x ( x = A -> B = C ) <-> [_ A / x ]_ B = C ) )