Metamath Proof Explorer

Theorem iblsubnc

Description: Choice-free analogue of iblsub . (Contributed by Brendan Leahy, 11-Nov-2017)

Ref Expression
Hypotheses ibladdnc.1 ⊢ φ ∧ x ∈ A → B ∈ V
ibladdnc.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
ibladdnc.3 ⊢ φ ∧ x ∈ A → C ∈ V
ibladdnc.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
iblsubnc.m ⊢ φ → x ∈ A ⟼ B − C ∈ MblFn
Assertion iblsubnc ⊢ φ → x ∈ A ⟼ B − C ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 ibladdnc.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 ibladdnc.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 ibladdnc.3 ⊢ φ ∧ x ∈ A → C ∈ V
4 ibladdnc.4 ⊢ φ → x ∈ A ⟼ C ∈ 𝐿 1
5 iblsubnc.m ⊢ φ → x ∈ A ⟼ B − C ∈ MblFn
6 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
7 2 6 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
8 7 1 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
9 iblmbf ⊢ x ∈ A ⟼ C ∈ 𝐿 1 → x ∈ A ⟼ C ∈ MblFn
10 4 9 syl ⊢ φ → x ∈ A ⟼ C ∈ MblFn
11 10 3 mbfmptcl ⊢ φ ∧ x ∈ A → C ∈ ℂ
12 8 11 negsubd ⊢ φ ∧ x ∈ A → B + − C = B − C
13 12 mpteq2dva ⊢ φ → x ∈ A ⟼ B + − C = x ∈ A ⟼ B − C
14 11 negcld ⊢ φ ∧ x ∈ A → − C ∈ ℂ
15 3 4 iblneg ⊢ φ → x ∈ A ⟼ − C ∈ 𝐿 1
16 13 5 eqeltrd ⊢ φ → x ∈ A ⟼ B + − C ∈ MblFn
17 8 2 14 15 16 ibladdnc ⊢ φ → x ∈ A ⟼ B + − C ∈ 𝐿 1
18 13 17 eqeltrrd ⊢ φ → x ∈ A ⟼ B − C ∈ 𝐿 1