Metamath Proof Explorer

Theorem csbif

Description: Distribute proper substitution through the conditional operator. (Contributed by NM, 24-Feb-2013) (Revised by NM, 19-Aug-2018)

Ref Expression
Assertion csbif ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) )
2 dfsbcq2 ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4 csbeq1 ⊢ ( 𝑦 = 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
5 2 3 4 ifbieq12d ⊢ ( 𝑦 = 𝐴 → if ( [ 𝑦 / 𝑥 ] 𝜑 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
6 1 5 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ⦋ 𝑦 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝑦 / 𝑥 ] 𝜑 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
7 vex ⊢ 𝑦 ∈ V
8 nfs1v ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
9 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
10 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
11 8 9 10 nfif ⊢ Ⅎ 𝑥 if ( [ 𝑦 / 𝑥 ] 𝜑 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
12 sbequ12 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
13 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
15 12 13 14 ifbieq12d ⊢ ( 𝑥 = 𝑦 → if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝑦 / 𝑥 ] 𝜑 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
16 7 11 15 csbief ⊢ ⦋ 𝑦 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝑦 / 𝑥 ] 𝜑 , ⦋ 𝑦 / 𝑥 ⦌ 𝐵 , ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
17 6 16 vtoclg ⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
18 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = ∅ )
19 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ∅ )
20 csbprc ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 = ∅ )
21 19 20 ifeq12d ⊢ ( ¬ 𝐴 ∈ V → if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ∅ , ∅ ) )
22 ifid ⊢ if ( [ 𝐴 / 𝑥 ] 𝜑 , ∅ , ∅ ) = ∅
23 21 22 eqtr2di ⊢ ( ¬ 𝐴 ∈ V → ∅ = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
24 18 23 eqtrd ⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
25 17 24 pm2.61i ⊢ ⦋ 𝐴 / 𝑥 ⦌ if ( 𝜑 , 𝐵 , 𝐶 ) = if ( [ 𝐴 / 𝑥 ] 𝜑 , ⦋ 𝐴 / 𝑥 ⦌ 𝐵 , ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )