Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Recursive definition generator
rdgsucmpt
Metamath Proof Explorer
Description: The value of the recursive definition generator at a successor (special
case where the characteristic function uses the map operation).
(Contributed by Mario Carneiro , 9-Sep-2013)
Ref
Expression
Hypotheses
rdgsucmpt.1
⊢ F = rec ⁡ x ∈ V ⟼ C A
rdgsucmpt.2
⊢ x = F ⁡ B → C = D
Assertion
rdgsucmpt
⊢ B ∈ On ∧ D ∈ V → F ⁡ suc ⁡ B = D
Proof
Step
Hyp
Ref
Expression
1
rdgsucmpt.1
⊢ F = rec ⁡ x ∈ V ⟼ C A
2
rdgsucmpt.2
⊢ x = F ⁡ B → C = D
3
nfcv
⊢ Ⅎ _ x A
4
nfcv
⊢ Ⅎ _ x B
5
nfcv
⊢ Ⅎ _ x D
6
3 4 5 1 2
rdgsucmptf
⊢ B ∈ On ∧ D ∈ V → F ⁡ suc ⁡ B = D