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 ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    𝐴 ∈ 𝑉    ▶    𝐴 ∈ 𝑉    )
2 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
3 1 2 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 )    )
4 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
5 4 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
6 1 5 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )    )
7 pm4.38 ⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) ∧ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
8 7 ex ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) → ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) )
9 3 6 8 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )    )
10 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) )
11 10 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ) )
12 1 11 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) )    )
13 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) )
14 13 biimprcd ⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑦 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) )
15 9 12 14 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )    )
16 15 gen11 ⊢ (    𝐴 ∈ 𝑉    ▶    ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )    )
17 exbi ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) → ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) )
18 16 17 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )    )
19 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
20 19 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) )
21 1 20 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )    )
22 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ↔ ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) )
23 22 biimprcd ⊢ ( ( ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) → ( ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ) → ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ) )
24 18 21 23 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )    )
25 24 gen11 ⊢ (    𝐴 ∈ 𝑉    ▶    ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )    )
26 abbi ⊢ ( ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) ↔ { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } )
27 26 biimpi ⊢ ( ∀ 𝑧 ( [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) ) → { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } )
28 25 27 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) }    )
29 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }
30 29 a1i ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } )
31 1 30 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }    )
32 eqeq2 ⊢ ( { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } ) )
33 32 biimpd ⊢ ( { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } → ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } ) )
34 28 31 33 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) }    )
35 df-uni ⊢ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }
36 35 ax-gen ⊢ ∀ 𝑥 ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }
37 spsbc ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } → [ 𝐴 / 𝑥 ] ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } ) )
38 1 36 37 e10 ⊢ (    𝐴 ∈ 𝑉    ▶    [ 𝐴 / 𝑥 ] ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }    )
39 sbceqg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } ) )
40 39 biimpd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } ) )
41 1 38 40 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) }    )
42 eqeq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } ) )
43 42 biimpd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) } → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } ) )
44 34 41 43 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) }    )
45 df-uni ⊢ ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) }
46 eqeq2 ⊢ ( ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } ) )
47 46 biimprcd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ( ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) } → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ) )
48 44 45 47 e10 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵    )
49 48 in1 ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∪ 𝐵 = ∪ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )