Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
ifov
Next ⟩
dmoprab
Metamath Proof Explorer
Ascii
Unicode
Theorem
ifov
Description:
Move a conditional outside of an operation.
(Contributed by
AV
, 11-Nov-2019)
Ref
Expression
Assertion
ifov
⊢
A
if
φ
F
G
B
=
if
φ
A
F
B
A
G
B
Proof
Step
Hyp
Ref
Expression
1
oveq
⊢
if
φ
F
G
=
F
→
A
if
φ
F
G
B
=
A
F
B
2
oveq
⊢
if
φ
F
G
=
G
→
A
if
φ
F
G
B
=
A
G
B
3
1
2
ifsb
⊢
A
if
φ
F
G
B
=
if
φ
A
F
B
A
G
B