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 AVA/xB=A/xB

Proof

Step Hyp Ref Expression
1 idn1 AVAV
2 sbceqg AV[˙A/x]˙y=BA/xy=A/xB
3 1 2 e1a AV[˙A/x]˙y=BA/xy=A/xB
4 csbconstg AVA/xy=y
5 1 4 e1a AVA/xy=y
6 eqeq1 A/xy=yA/xy=A/xBy=A/xB
7 5 6 e1a AVA/xy=A/xBy=A/xB
8 bibi1 [˙A/x]˙y=BA/xy=A/xB[˙A/x]˙y=By=A/xBA/xy=A/xBy=A/xB
9 8 biimprd [˙A/x]˙y=BA/xy=A/xBA/xy=A/xBy=A/xB[˙A/x]˙y=By=A/xB
10 3 7 9 e11 AV[˙A/x]˙y=By=A/xB
11 10 gen11 AVy[˙A/x]˙y=By=A/xB
12 abbi y[˙A/x]˙y=By=A/xBy|[˙A/x]˙y=B=y|y=A/xB
13 12 biimpi y[˙A/x]˙y=By=A/xBy|[˙A/x]˙y=B=y|y=A/xB
14 11 13 e1a AVy|[˙A/x]˙y=B=y|y=A/xB
15 csbab A/xy|y=B=y|[˙A/x]˙y=B
16 15 a1i AVA/xy|y=B=y|[˙A/x]˙y=B
17 16 eqcomd AVy|[˙A/x]˙y=B=A/xy|y=B
18 1 17 e1a AVy|[˙A/x]˙y=B=A/xy|y=B
19 eqeq1 y|[˙A/x]˙y=B=A/xy|y=By|[˙A/x]˙y=B=y|y=A/xBA/xy|y=B=y|y=A/xB
20 19 biimpcd y|[˙A/x]˙y=B=y|y=A/xBy|[˙A/x]˙y=B=A/xy|y=BA/xy|y=B=y|y=A/xB
21 14 18 20 e11 AVA/xy|y=B=y|y=A/xB
22 df-sn B=y|y=B
23 22 ax-gen xB=y|y=B
24 csbeq2 xB=y|y=BA/xB=A/xy|y=B
25 24 a1i AVxB=y|y=BA/xB=A/xy|y=B
26 1 23 25 e10 AVA/xB=A/xy|y=B
27 eqeq2 A/xy|y=B=y|y=A/xBA/xB=A/xy|y=BA/xB=y|y=A/xB
28 27 biimpd A/xy|y=B=y|y=A/xBA/xB=A/xy|y=BA/xB=y|y=A/xB
29 21 26 28 e11 AVA/xB=y|y=A/xB
30 df-sn A/xB=y|y=A/xB
31 eqeq2 A/xB=y|y=A/xBA/xB=A/xBA/xB=y|y=A/xB
32 31 biimprcd A/xB=y|y=A/xBA/xB=y|y=A/xBA/xB=A/xB
33 29 30 32 e10 AVA/xB=A/xB
34 33 in1 AVA/xB=A/xB