Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
csbov
Next ⟩
csbov12g
Metamath Proof Explorer
Ascii
Unicode
Theorem
csbov
Description:
Move class substitution in and out of an operation.
(Contributed by
NM
, 23-Aug-2018)
Ref
Expression
Assertion
csbov
⊢
⦋
A
/
x
⦌
B
F
C
=
B
⦋
A
/
x
⦌
F
C
Proof
Step
Hyp
Ref
Expression
1
csbov123
⊢
⦋
A
/
x
⦌
B
F
C
=
⦋
A
/
x
⦌
B
⦋
A
/
x
⦌
F
⦋
A
/
x
⦌
C
2
csbconstg
⊢
A
∈
V
→
⦋
A
/
x
⦌
B
=
B
3
csbconstg
⊢
A
∈
V
→
⦋
A
/
x
⦌
C
=
C
4
2
3
oveq12d
⊢
A
∈
V
→
⦋
A
/
x
⦌
B
⦋
A
/
x
⦌
F
⦋
A
/
x
⦌
C
=
B
⦋
A
/
x
⦌
F
C
5
0fv
⊢
∅
⁡
B
C
=
∅
6
df-ov
⊢
B
∅
C
=
∅
⁡
B
C
7
0ov
⊢
⦋
A
/
x
⦌
B
∅
⦋
A
/
x
⦌
C
=
∅
8
5
6
7
3eqtr4ri
⊢
⦋
A
/
x
⦌
B
∅
⦋
A
/
x
⦌
C
=
B
∅
C
9
csbprc
⊢
¬
A
∈
V
→
⦋
A
/
x
⦌
F
=
∅
10
9
oveqd
⊢
¬
A
∈
V
→
⦋
A
/
x
⦌
B
⦋
A
/
x
⦌
F
⦋
A
/
x
⦌
C
=
⦋
A
/
x
⦌
B
∅
⦋
A
/
x
⦌
C
11
9
oveqd
⊢
¬
A
∈
V
→
B
⦋
A
/
x
⦌
F
C
=
B
∅
C
12
8
10
11
3eqtr4a
⊢
¬
A
∈
V
→
⦋
A
/
x
⦌
B
⦋
A
/
x
⦌
F
⦋
A
/
x
⦌
C
=
B
⦋
A
/
x
⦌
F
C
13
4
12
pm2.61i
⊢
⦋
A
/
x
⦌
B
⦋
A
/
x
⦌
F
⦋
A
/
x
⦌
C
=
B
⦋
A
/
x
⦌
F
C
14
1
13
eqtri
⊢
⦋
A
/
x
⦌
B
F
C
=
B
⦋
A
/
x
⦌
F
C