Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Functions
iffv
Next ⟩
fv3
Metamath Proof Explorer
Ascii
Unicode
Theorem
iffv
Description:
Move a conditional outside of a function.
(Contributed by
Thierry Arnoux
, 28-Sep-2018)
Ref
Expression
Assertion
iffv
⊢
if
φ
F
G
⁡
A
=
if
φ
F
⁡
A
G
⁡
A
Proof
Step
Hyp
Ref
Expression
1
fveq1
⊢
if
φ
F
G
=
F
→
if
φ
F
G
⁡
A
=
F
⁡
A
2
fveq1
⊢
if
φ
F
G
=
G
→
if
φ
F
G
⁡
A
=
G
⁡
A
3
1
2
ifsb
⊢
if
φ
F
G
⁡
A
=
if
φ
F
⁡
A
G
⁡
A