Metamath Proof Explorer

Theorem csbunigVD

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

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

Ref Expression
Assertion csbunigVD ⊢A∈V→⦋A/x⦌⋃B=⋃⦋A/x⦌B

Proof

Step Hyp Ref Expression
1 idn1 ⊢A∈V→A∈V
2 sbcg ⊢A∈V→[˙A/x]˙z∈y↔z∈y
3 1 2 e1a ⊢A∈V→[˙A/x]˙z∈y↔z∈y
4 sbcel2 ⊢[˙A/x]˙y∈B↔y∈⦋A/x⦌B
5 4 a1i ⊢A∈V→[˙A/x]˙y∈B↔y∈⦋A/x⦌B
6 1 5 e1a ⊢A∈V→[˙A/x]˙y∈B↔y∈⦋A/x⦌B
7 pm4.38 ⊢[˙A/x]˙z∈y↔z∈y∧[˙A/x]˙y∈B↔y∈⦋A/x⦌B→[˙A/x]˙z∈y∧[˙A/x]˙y∈B↔z∈y∧y∈⦋A/x⦌B
8 7 ex ⊢[˙A/x]˙z∈y↔z∈y→[˙A/x]˙y∈B↔y∈⦋A/x⦌B→[˙A/x]˙z∈y∧[˙A/x]˙y∈B↔z∈y∧y∈⦋A/x⦌B
9 3 6 8 e11 ⊢A∈V→[˙A/x]˙z∈y∧[˙A/x]˙y∈B↔z∈y∧y∈⦋A/x⦌B
10 sbcan ⊢[˙A/x]˙z∈y∧y∈B↔[˙A/x]˙z∈y∧[˙A/x]˙y∈B
11 10 a1i ⊢A∈V→[˙A/x]˙z∈y∧y∈B↔[˙A/x]˙z∈y∧[˙A/x]˙y∈B
12 1 11 e1a ⊢A∈V→[˙A/x]˙z∈y∧y∈B↔[˙A/x]˙z∈y∧[˙A/x]˙y∈B
13 bibi1 ⊢[˙A/x]˙z∈y∧y∈B↔[˙A/x]˙z∈y∧[˙A/x]˙y∈B→[˙A/x]˙z∈y∧y∈B↔z∈y∧y∈⦋A/x⦌B↔[˙A/x]˙z∈y∧[˙A/x]˙y∈B↔z∈y∧y∈⦋A/x⦌B
14 13 biimprcd ⊢[˙A/x]˙z∈y∧[˙A/x]˙y∈B↔z∈y∧y∈⦋A/x⦌B→[˙A/x]˙z∈y∧y∈B↔[˙A/x]˙z∈y∧[˙A/x]˙y∈B→[˙A/x]˙z∈y∧y∈B↔z∈y∧y∈⦋A/x⦌B
15 9 12 14 e11 ⊢A∈V→[˙A/x]˙z∈y∧y∈B↔z∈y∧y∈⦋A/x⦌B
16 15 gen11 ⊢A∈V→∀y[˙A/x]˙z∈y∧y∈B↔z∈y∧y∈⦋A/x⦌B
17 exbi ⊢∀y[˙A/x]˙z∈y∧y∈B↔z∈y∧y∈⦋A/x⦌B→∃y[˙A/x]˙z∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
18 16 17 e1a ⊢A∈V→∃y[˙A/x]˙z∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
19 sbcex2 ⊢[˙A/x]˙∃yz∈y∧y∈B↔∃y[˙A/x]˙z∈y∧y∈B
20 19 a1i ⊢A∈V→[˙A/x]˙∃yz∈y∧y∈B↔∃y[˙A/x]˙z∈y∧y∈B
21 1 20 e1a ⊢A∈V→[˙A/x]˙∃yz∈y∧y∈B↔∃y[˙A/x]˙z∈y∧y∈B
22 bibi1 ⊢[˙A/x]˙∃yz∈y∧y∈B↔∃y[˙A/x]˙z∈y∧y∈B→[˙A/x]˙∃yz∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B↔∃y[˙A/x]˙z∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
23 22 biimprcd ⊢∃y[˙A/x]˙z∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B→[˙A/x]˙∃yz∈y∧y∈B↔∃y[˙A/x]˙z∈y∧y∈B→[˙A/x]˙∃yz∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
24 18 21 23 e11 ⊢A∈V→[˙A/x]˙∃yz∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
25 24 gen11 ⊢A∈V→∀z[˙A/x]˙∃yz∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
26 abbib ⊢z|[˙A/x]˙∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B↔∀z[˙A/x]˙∃yz∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B
27 26 biimpri ⊢∀z[˙A/x]˙∃yz∈y∧y∈B↔∃yz∈y∧y∈⦋A/x⦌B→z|[˙A/x]˙∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B
28 25 27 e1a ⊢A∈V→z|[˙A/x]˙∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B
29 csbab ⊢⦋A/x⦌z|∃yz∈y∧y∈B=z|[˙A/x]˙∃yz∈y∧y∈B
30 29 a1i ⊢A∈V→⦋A/x⦌z|∃yz∈y∧y∈B=z|[˙A/x]˙∃yz∈y∧y∈B
31 1 30 e1a ⊢A∈V→⦋A/x⦌z|∃yz∈y∧y∈B=z|[˙A/x]˙∃yz∈y∧y∈B
32 eqeq2 ⊢z|[˙A/x]˙∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B→⦋A/x⦌z|∃yz∈y∧y∈B=z|[˙A/x]˙∃yz∈y∧y∈B↔⦋A/x⦌z|∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B
33 32 biimpd ⊢z|[˙A/x]˙∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B→⦋A/x⦌z|∃yz∈y∧y∈B=z|[˙A/x]˙∃yz∈y∧y∈B→⦋A/x⦌z|∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B
34 28 31 33 e11 ⊢A∈V→⦋A/x⦌z|∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B
35 df-uni ⊢⋃B=z|∃yz∈y∧y∈B
36 35 ax-gen ⊢∀x⋃B=z|∃yz∈y∧y∈B
37 spsbc ⊢A∈V→∀x⋃B=z|∃yz∈y∧y∈B→[˙A/x]˙⋃B=z|∃yz∈y∧y∈B
38 1 36 37 e10 ⊢A∈V→[˙A/x]˙⋃B=z|∃yz∈y∧y∈B
39 sbceqg ⊢A∈V→[˙A/x]˙⋃B=z|∃yz∈y∧y∈B↔⦋A/x⦌⋃B=⦋A/x⦌z|∃yz∈y∧y∈B
40 39 biimpd ⊢A∈V→[˙A/x]˙⋃B=z|∃yz∈y∧y∈B→⦋A/x⦌⋃B=⦋A/x⦌z|∃yz∈y∧y∈B
41 1 38 40 e11 ⊢A∈V→⦋A/x⦌⋃B=⦋A/x⦌z|∃yz∈y∧y∈B
42 eqeq2 ⊢⦋A/x⦌z|∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B→⦋A/x⦌⋃B=⦋A/x⦌z|∃yz∈y∧y∈B↔⦋A/x⦌⋃B=z|∃yz∈y∧y∈⦋A/x⦌B
43 42 biimpd ⊢⦋A/x⦌z|∃yz∈y∧y∈B=z|∃yz∈y∧y∈⦋A/x⦌B→⦋A/x⦌⋃B=⦋A/x⦌z|∃yz∈y∧y∈B→⦋A/x⦌⋃B=z|∃yz∈y∧y∈⦋A/x⦌B
44 34 41 43 e11 ⊢A∈V→⦋A/x⦌⋃B=z|∃yz∈y∧y∈⦋A/x⦌B
45 df-uni ⊢⋃⦋A/x⦌B=z|∃yz∈y∧y∈⦋A/x⦌B
46 eqeq2 ⊢⋃⦋A/x⦌B=z|∃yz∈y∧y∈⦋A/x⦌B→⦋A/x⦌⋃B=⋃⦋A/x⦌B↔⦋A/x⦌⋃B=z|∃yz∈y∧y∈⦋A/x⦌B
47 46 biimprcd ⊢⦋A/x⦌⋃B=z|∃yz∈y∧y∈⦋A/x⦌B→⋃⦋A/x⦌B=z|∃yz∈y∧y∈⦋A/x⦌B→⦋A/x⦌⋃B=⋃⦋A/x⦌B
48 44 45 47 e10 ⊢A∈V→⦋A/x⦌⋃B=⋃⦋A/x⦌B
49 48 in1 ⊢A∈V→⦋A/x⦌⋃B=⋃⦋A/x⦌B