findabrcl

Description: Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008) (Revised by Mario Carneiro, 11-Sep-2015)

		Ref	Expression
	Hypothesis	findabrcl.1	$⊢ z \in P \to G (z) \in P$
	Assertion	findabrcl	$⊢ (C \in ω \land A \in P) \to (x \in V ⟼ rec (G, A) (x)) (C) \in P$

Step	Hyp	Ref	Expression
1		findabrcl.1	$⊢ z \in P \to G (z) \in P$
2		elex	$⊢ C \in ω \to C \in V$
3		fveq2	$⊢ x = C \to rec (G, A) (x) = rec (G, A) (C)$
4		eqid	$⊢ (x \in V ⟼ rec (G, A) (x)) = (x \in V ⟼ rec (G, A) (x))$
5		fvex	$⊢ rec (G, A) (C) \in V$
6	3 4 5	fvmpt	$⊢ C \in V \to (x \in V ⟼ rec (G, A) (x)) (C) = rec (G, A) (C)$
7	2 6	syl	$⊢ C \in ω \to (x \in V ⟼ rec (G, A) (x)) (C) = rec (G, A) (C)$
8	7	adantr	$⊢ (C \in ω \land A \in P) \to (x \in V ⟼ rec (G, A) (x)) (C) = rec (G, A) (C)$
9	1	findreccl	$⊢ C \in ω \to (A \in P \to rec (G, A) (C) \in P)$
10	9	imp	$⊢ (C \in ω \land A \in P) \to rec (G, A) (C) \in P$
11	8 10	eqeltrd	$⊢ (C \in ω \land A \in P) \to (x \in V ⟼ rec (G, A) (x)) (C) \in P$

Metamath Proof Explorer