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

Metamath Proof Explorer

Theorem elpreqprlem

Description: Lemma for elpreqpr . (Contributed by Scott Fenton, 7-Dec-2020) (Revised by AV, 9-Dec-2020)

Ref Expression
Assertion elpreqprlem 
|- ( B e. V -> E. x { B , C } = { B , x } )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { B , C } = { B , C }
2 preq2 
 |-  ( x = C -> { B , x } = { B , C } )
3 2 eqeq2d 
 |-  ( x = C -> ( { B , C } = { B , x } <-> { B , C } = { B , C } ) )
4 3 spcegv 
 |-  ( C e. _V -> ( { B , C } = { B , C } -> E. x { B , C } = { B , x } ) )
5 1 4 mpi 
 |-  ( C e. _V -> E. x { B , C } = { B , x } )
6 5 a1d 
 |-  ( C e. _V -> ( B e. V -> E. x { B , C } = { B , x } ) )
7 dfsn2 
 |-  { B } = { B , B }
8 preq2 
 |-  ( x = B -> { B , x } = { B , B } )
9 8 eqeq2d 
 |-  ( x = B -> ( { B } = { B , x } <-> { B } = { B , B } ) )
10 9 spcegv 
 |-  ( B e. V -> ( { B } = { B , B } -> E. x { B } = { B , x } ) )
11 7 10 mpi 
 |-  ( B e. V -> E. x { B } = { B , x } )
12 prprc2 
 |-  ( -. C e. _V -> { B , C } = { B } )
13 12 eqeq1d 
 |-  ( -. C e. _V -> ( { B , C } = { B , x } <-> { B } = { B , x } ) )
14 13 exbidv 
 |-  ( -. C e. _V -> ( E. x { B , C } = { B , x } <-> E. x { B } = { B , x } ) )
15 11 14 imbitrrid 
 |-  ( -. C e. _V -> ( B e. V -> E. x { B , C } = { B , x } ) )
16 6 15 pm2.61i 
 |-  ( B e. V -> E. x { B , C } = { B , x } )