Metamath Proof Explorer

Theorem csbingVD

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

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

Ref Expression
Assertion csbingVD ( 𝐴 ∈ 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
2 df-in ⊢ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }
3 2 ax-gen ⊢ ∀ 𝑥 ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }
4 spsbc ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → [ 𝐴 / 𝑥 ] ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) )
5 1 3 4 e10 ⊢ (    𝐴 ∈ 𝐵    ▶    [ 𝐴 / 𝑥 ] ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }    )
6 sbceqg ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) )
7 6 biimpd ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) )
8 1 5 7 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }    )
9 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }
10 9 a1i ⊢ ( 𝐴 ∈ 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } )
11 1 10 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }    )
12 eqeq1 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ↔ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) )
13 12 biimprd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } ) )
14 8 11 13 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) }    )
15 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) )
16 15 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ) )
17 1 16 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) )    )
18 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
19 18 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
20 1 19 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )    )
21 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 )
22 21 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )
23 1 22 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 )    )
24 pm4.38 ⊢ ( ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ∧ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) )
25 24 ex ⊢ ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) ) )
26 20 23 25 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )    )
27 bibi1 ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ) → ( ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) ↔ ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) ) )
28 27 biimprd ⊢ ( ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ) → ( ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ∧ [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) ) )
29 17 26 28 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )    )
30 29 gen11 ⊢ (    𝐴 ∈ 𝐵    ▶    ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )    )
31 abbib ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } ↔ ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) )
32 31 biimpri ⊢ ( ∀ 𝑦 ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) → { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } )
33 30 32 e1a ⊢ (    𝐴 ∈ 𝐵    ▶    { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) }    )
34 eqeq1 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } ) )
35 34 biimprd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } → ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) } = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } ) )
36 14 33 35 e11 ⊢ (    𝐴 ∈ 𝐵    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) }    )
37 df-in ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) }
38 eqeq2 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } ) )
39 38 biimprcd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) = { 𝑦 ∣ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∧ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) } → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) ) )
40 36 37 39 e10 ⊢ (    𝐴 ∈ 𝐵    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 )    )
41 40 in1 ⊢ ( 𝐴 ∈ 𝐵 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 ∩ 𝐷 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∩ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ) )