# Metamath Proof Explorer

## Theorem csbxpgVD

Description: Virtual deduction proof of csbxp . 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. csbxp is csbxpgVD without virtual deductions and was automatically derived from csbxpgVD .

 1:: |- (. A e. V ->. A e. V ). 2:1: |- (. A e. V ->. ( [. A / x ]. w e. B <-> [_ A / x ]_ w e. [_ A / x ]_ B ) ). 3:1: |- (. A e. V ->. [_ A / x ]_ w = w ). 4:3: |- (. A e. V ->. ( [_ A / x ]_ w e. [_ A / x ]_ B <-> w e. [_ A / x ]_ B ) ). 5:2,4: |- (. A e. V ->. ( [. A / x ]. w e. B <-> w e. [_ A / x ]_ B ) ). 6:1: |- (. A e. V ->. ( [. A / x ]. y e. C <-> [_ A / x ]_ y e. [_ A / x ]_ C ) ). 7:1: |- (. A e. V ->. [_ A / x ]_ y = y ). 8:7: |- (. A e. V ->. ( [_ A / x ]_ y e. [_ A / x ]_ C <-> y e. [_ A / x ]_ C ) ). 9:6,8: |- (. A e. V ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ). 10:5,9: |- (. A e. V ->. ( ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ). 11:1: |- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( [. A / x ]. w e. B /\ [. A / x ]. y e. C ) ) ). 12:10,11: |- (. A e. V ->. ( [. A / x ]. ( w e. B /\ y e. C ) <-> ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ). 13:1: |- (. A e. V ->. ( [. A / x ]. z = <. w ,. y >. <-> z = <. w , y >. ) ). 14:12,13: |- (. A e. V ->. ( ( [. A / x ]. z = <. w ,. y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 15:1: |- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( [. A / x ]. z = <. w , y >. /\ [. A / x ]. ( w e. B /\ y e. C ) ) ) ). 16:14,15: |- (. A e. V ->. ( [. A / x ]. ( z = <. w ,. y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 17:16: |- (. A e. V ->. A. y ( [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 18:17: |- (. A e. V ->. ( E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 19:1: |- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y [. A / x ]. ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ). 20:18,19: |- (. A e. V ->. ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 21:20: |- (. A e. V ->. A. w ( [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 22:21: |- (. A e. V ->. ( E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 23:1: |- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w [. A / x ]. E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) ) ). 24:22,23: |- (. A e. V ->. ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 25:24: |- (. A e. V ->. A. z ( [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) <-> E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) ) ). 26:25: |- (. A e. V ->. { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ). 27:1: |- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | [. A / x ]. E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ). 28:26,27: |- (. A e. V ->. [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ). 29:: |- { <. w ,. y >. | ( w e. B /\ y e. C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } 30:: |- ( B X. C ) = { <. w ,. y >. | ( w e. B /\ y e. C ) } 31:29,30: |- ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } 32:31: |- A. x ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } 33:1,32: |- (. A e. V ->. [_ A / x ]_ ( B X. C ) = [_ A / x ]_ { z | E. w E. y ( z = <. w , y >. /\ ( w e. B /\ y e. C ) ) } ). 34:28,33: |- (. A e. V ->. [_ A / x ]_ ( B X. C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } ). 35:: |- { <. w ,. y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } 36:: |- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { <. w , y >. | ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) } 37:35,36: |- ( [_ A / x ]_ B X. [_ A / x ]_ C ) = { z | E. w E. y ( z = <. w , y >. /\ ( w e. [_ A / x ]_ B /\ y e. [_ A / x ]_ C ) ) } 38:34,37: |- (. A e. V ->. [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) ). qed:38: |- ( A e. V -> [_ A / x ]_ ( B X. C ) = ( [_ A / x ]_ B X. [_ A / x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbxpgVD

### Proof

Step Hyp Ref Expression
1 idn1 ${⊢}\left({A}\in {V}{\to }{A}\in {V}\right)$
2 sbcel12
3 2 a1i
4 1 3 e1a
5 csbconstg
6 1 5 e1a
7 eleq1
8 6 7 e1a
9 bibi1
10 9 biimprd
11 4 8 10 e11
12 sbcel12
13 12 a1i
14 1 13 e1a
15 csbconstg
16 1 15 e1a
17 eleq1
18 16 17 e1a
19 bibi1
20 19 biimprd
21 14 18 20 e11
22 pm4.38
23 22 ex
24 11 21 23 e11
25 sbcan
26 25 a1i
27 1 26 e1a
28 bibi1
29 28 biimprcd
30 24 27 29 e11
31 sbcg
32 1 31 e1a
33 pm4.38
34 33 expcom
35 30 32 34 e11
36 sbcan
37 36 a1i
38 1 37 e1a
39 bibi1
40 39 biimprcd
41 35 38 40 e11
42 41 gen11
43 exbi
44 42 43 e1a
45 sbcex2
46 45 a1i
47 1 46 e1a
48 bibi1
49 48 biimprcd
50 44 47 49 e11
51 50 gen11
52 exbi
53 51 52 e1a
54 sbcex2
55 54 a1i
56 1 55 e1a
57 bibi1
58 57 biimprcd
59 53 56 58 e11
60 59 gen11
61 abbi
62 61 biimpi
63 60 62 e1a
64 csbab
65 64 a1i
66 1 65 e1a
67 eqeq2
68 67 biimpd
69 63 66 68 e11
70 df-xp ${⊢}{B}×{C}=\left\{⟨{w},{y}⟩|\left({w}\in {B}\wedge {y}\in {C}\right)\right\}$
71 df-opab ${⊢}\left\{⟨{w},{y}⟩|\left({w}\in {B}\wedge {y}\in {C}\right)\right\}=\left\{{z}|\exists {w}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{w},{y}⟩\wedge \left({w}\in {B}\wedge {y}\in {C}\right)\right)\right\}$
72 70 71 eqtri ${⊢}{B}×{C}=\left\{{z}|\exists {w}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{w},{y}⟩\wedge \left({w}\in {B}\wedge {y}\in {C}\right)\right)\right\}$
73 72 ax-gen ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{B}×{C}=\left\{{z}|\exists {w}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({z}=⟨{w},{y}⟩\wedge \left({w}\in {B}\wedge {y}\in {C}\right)\right)\right\}$
74 csbeq2
75 74 a1i
76 1 73 75 e10
77 eqeq2
78 77 biimpd
79 69 76 78 e11
80 df-xp
81 df-opab
82 80 81 eqtri
83 eqeq2
84 83 biimprcd
85 79 82 84 e10
86 85 in1