# Metamath Proof Explorer

## Theorem csbsngVD

Description: Virtual deduction proof of csbsng . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbsng is csbsngVD without virtual deductions and was automatically derived from csbsngVD .

 1:: |- (. A e. V ->. A e. V ). 2:1: |- (. A e. V ->. ( [. A / x ]. y = B <-> [_ A / x ]_ y = [_ A / x ]_ B ) ). 3:1: |- (. A e. V ->. [_ A / x ]_ y = y ). 4:3: |- (. A e. V ->. ( [_ A / x ]_ y = [_ A / x ]_ B <-> y = [_ A / x ]_ B ) ). 5:2,4: |- (. A e. V ->. ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ). 6:5: |- (. A e. V ->. A. y ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ). 7:6: |- (. A e. V ->. { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } ). 8:1: |- (. A e. V ->. { y | [. A / x ]. y = B } = [_ A / x ]_ { y | y = B } ). 9:7,8: |- (. A e. V ->. [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } ). 10:: |- { B } = { y | y = B } 11:10: |- A. x { B } = { y | y = B } 12:1,11: |- (. A e. V ->. [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } ). 13:9,12: |- (. A e. V ->. [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } ). 14:: |- { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B } 15:13,14: |- (. A e. V ->. [_ A / x ]_ { B } = { [_ A / x ]_ B } ). qed:15: |- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbsngVD
`|- ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )`

### Proof

Step Hyp Ref Expression
1 idn1
` |-  (. A e. V ->. A e. V ).`
2 sbceqg
` |-  ( A e. V -> ( [. A / x ]. y = B <-> [_ A / x ]_ y = [_ A / x ]_ B ) )`
3 1 2 e1a
` |-  (. A e. V ->. ( [. A / x ]. y = B <-> [_ A / x ]_ y = [_ A / x ]_ B ) ).`
4 csbconstg
` |-  ( A e. V -> [_ A / x ]_ y = y )`
5 1 4 e1a
` |-  (. A e. V ->. [_ A / x ]_ y = y ).`
6 eqeq1
` |-  ( [_ A / x ]_ y = y -> ( [_ A / x ]_ y = [_ A / x ]_ B <-> y = [_ A / x ]_ B ) )`
7 5 6 e1a
` |-  (. A e. V ->. ( [_ A / x ]_ y = [_ A / x ]_ B <-> y = [_ A / x ]_ B ) ).`
8 bibi1
` |-  ( ( [. A / x ]. y = B <-> [_ A / x ]_ y = [_ A / x ]_ B ) -> ( ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) <-> ( [_ A / x ]_ y = [_ A / x ]_ B <-> y = [_ A / x ]_ B ) ) )`
9 8 biimprd
` |-  ( ( [. A / x ]. y = B <-> [_ A / x ]_ y = [_ A / x ]_ B ) -> ( ( [_ A / x ]_ y = [_ A / x ]_ B <-> y = [_ A / x ]_ B ) -> ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ) )`
10 3 7 9 e11
` |-  (. A e. V ->. ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ).`
11 10 gen11
` |-  (. A e. V ->. A. y ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) ).`
12 abbi
` |-  ( A. y ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) <-> { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } )`
13 12 biimpi
` |-  ( A. y ( [. A / x ]. y = B <-> y = [_ A / x ]_ B ) -> { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } )`
14 11 13 e1a
` |-  (. A e. V ->. { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } ).`
15 csbab
` |-  [_ A / x ]_ { y | y = B } = { y | [. A / x ]. y = B }`
16 15 a1i
` |-  ( A e. V -> [_ A / x ]_ { y | y = B } = { y | [. A / x ]. y = B } )`
17 16 eqcomd
` |-  ( A e. V -> { y | [. A / x ]. y = B } = [_ A / x ]_ { y | y = B } )`
18 1 17 e1a
` |-  (. A e. V ->. { y | [. A / x ]. y = B } = [_ A / x ]_ { y | y = B } ).`
19 eqeq1
` |-  ( { y | [. A / x ]. y = B } = [_ A / x ]_ { y | y = B } -> ( { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } <-> [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } ) )`
20 19 biimpcd
` |-  ( { y | [. A / x ]. y = B } = { y | y = [_ A / x ]_ B } -> ( { y | [. A / x ]. y = B } = [_ A / x ]_ { y | y = B } -> [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } ) )`
21 14 18 20 e11
` |-  (. A e. V ->. [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } ).`
22 df-sn
` |-  { B } = { y | y = B }`
23 22 ax-gen
` |-  A. x { B } = { y | y = B }`
24 csbeq2
` |-  ( A. x { B } = { y | y = B } -> [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } )`
25 24 a1i
` |-  ( A e. V -> ( A. x { B } = { y | y = B } -> [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } ) )`
26 1 23 25 e10
` |-  (. A e. V ->. [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } ).`
27 eqeq2
` |-  ( [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } -> ( [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } <-> [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } ) )`
28 27 biimpd
` |-  ( [_ A / x ]_ { y | y = B } = { y | y = [_ A / x ]_ B } -> ( [_ A / x ]_ { B } = [_ A / x ]_ { y | y = B } -> [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } ) )`
29 21 26 28 e11
` |-  (. A e. V ->. [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } ).`
30 df-sn
` |-  { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B }`
31 eqeq2
` |-  ( { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B } -> ( [_ A / x ]_ { B } = { [_ A / x ]_ B } <-> [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } ) )`
32 31 biimprcd
` |-  ( [_ A / x ]_ { B } = { y | y = [_ A / x ]_ B } -> ( { [_ A / x ]_ B } = { y | y = [_ A / x ]_ B } -> [_ A / x ]_ { B } = { [_ A / x ]_ B } ) )`
33 29 30 32 e10
` |-  (. A e. V ->. [_ A / x ]_ { B } = { [_ A / x ]_ B } ).`
34 33 in1
` |-  ( A e. V -> [_ A / x ]_ { B } = { [_ A / x ]_ B } )`