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