Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
Variable-to-class conversion for operations
caovdilem
Next ⟩
caovlem2
Metamath Proof Explorer
Ascii
Unicode
Theorem
caovdilem
Description:
Lemma used by real number construction.
(Contributed by
NM
, 26-Aug-1995)
Ref
Expression
Hypotheses
caovdir.1
⊢
A
∈
V
caovdir.2
⊢
B
∈
V
caovdir.3
⊢
C
∈
V
caovdir.com
⊢
x
G
y
=
y
G
x
caovdir.distr
⊢
x
G
y
F
z
=
x
G
y
F
x
G
z
caovdl.4
⊢
D
∈
V
caovdl.5
⊢
H
∈
V
caovdl.ass
⊢
x
G
y
G
z
=
x
G
y
G
z
Assertion
caovdilem
⊢
A
G
C
F
B
G
D
G
H
=
A
G
C
G
H
F
B
G
D
G
H
Proof
Step
Hyp
Ref
Expression
1
caovdir.1
⊢
A
∈
V
2
caovdir.2
⊢
B
∈
V
3
caovdir.3
⊢
C
∈
V
4
caovdir.com
⊢
x
G
y
=
y
G
x
5
caovdir.distr
⊢
x
G
y
F
z
=
x
G
y
F
x
G
z
6
caovdl.4
⊢
D
∈
V
7
caovdl.5
⊢
H
∈
V
8
caovdl.ass
⊢
x
G
y
G
z
=
x
G
y
G
z
9
ovex
⊢
A
G
C
∈
V
10
ovex
⊢
B
G
D
∈
V
11
9
10
7
4
5
caovdir
⊢
A
G
C
F
B
G
D
G
H
=
A
G
C
G
H
F
B
G
D
G
H
12
1
3
7
8
caovass
⊢
A
G
C
G
H
=
A
G
C
G
H
13
2
6
7
8
caovass
⊢
B
G
D
G
H
=
B
G
D
G
H
14
12
13
oveq12i
⊢
A
G
C
G
H
F
B
G
D
G
H
=
A
G
C
G
H
F
B
G
D
G
H
15
11
14
eqtri
⊢
A
G
C
F
B
G
D
G
H
=
A
G
C
G
H
F
B
G
D
G
H