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 A / x if φ B C = if [˙A / x]˙ φ A / x B A / x C

Proof

Step Hyp Ref Expression
1 csbeq1 y = A y / x if φ B C = A / x if φ B C
2 dfsbcq2 y = A y x φ [˙A / x]˙ φ
3 csbeq1 y = A y / x B = A / x B
4 csbeq1 y = A y / x C = A / x C
5 2 3 4 ifbieq12d y = A if y x φ y / x B y / x C = if [˙A / x]˙ φ A / x B A / x C
6 1 5 eqeq12d y = A y / x if φ B C = if y x φ y / x B y / x C A / x if φ B C = if [˙A / x]˙ φ A / x B A / x C
7 vex y V
8 nfs1v x y x φ
9 nfcsb1v _ x y / x B
10 nfcsb1v _ x y / x C
11 8 9 10 nfif _ x if y x φ y / x B y / x C
12 sbequ12 x = y φ y x φ
13 csbeq1a x = y B = y / x B
14 csbeq1a x = y C = y / x C
15 12 13 14 ifbieq12d x = y if φ B C = if y x φ y / x B y / x C
16 7 11 15 csbief y / x if φ B C = if y x φ y / x B y / x C
17 6 16 vtoclg A V A / x if φ B C = if [˙A / x]˙ φ A / x B A / x C
18 csbprc ¬ A V A / x if φ B C =
19 csbprc ¬ A V A / x B =
20 csbprc ¬ A V A / x C =
21 19 20 ifeq12d ¬ A V if [˙A / x]˙ φ A / x B A / x C = if [˙A / x]˙ φ
22 ifid if [˙A / x]˙ φ =
23 21 22 eqtr2di ¬ A V = if [˙A / x]˙ φ A / x B A / x C
24 18 23 eqtrd ¬ A V A / x if φ B C = if [˙A / x]˙ φ A / x B A / x C
25 17 24 pm2.61i A / x if φ B C = if [˙A / x]˙ φ A / x B A / x C