Theorem csbov2g 7435

Description: Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005.)

Assertion

Ref	Expression
csbov2g	⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))

Distinct variable groups:   𝑥,𝐵   𝑥,𝐹

Allowed substitution hints:   𝐴(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem csbov2g

Step	Hyp	Ref	Expression
1		csbov12g 7433	. 2 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
2		csbconstg 3881	. . 3 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌𝐵 = 𝐵)
3	2	oveq1d 7402	. 2 ⊢ (𝐴 ∈ 𝑉 → (⦋𝐴 / 𝑥⦌𝐵𝐹⦋𝐴 / 𝑥⦌𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))
4	1, 3	eqtrd 2764	1 ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵𝐹𝐶) = (𝐵𝐹⦋𝐴 / 𝑥⦌𝐶))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ⦋csb 3862  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  csbnegg  11418  prmgaplem7  17028  matgsum  22324  scmatscm  22400  pm2mpf1lem  22681  pm2mpcoe1  22687  pm2mpmhmlem2  22706  monmat2matmon  22711  divcncf  25348  logbmpt  26698  finxpreclem4  37382  tfsconcatfv  43330  cotrclrcl  43731  ply1mulgsumlem3  48377  ply1mulgsumlem4  48378  ply1mulgsum  48379