Theorem zfrepclf

Description: An inference based on the Axiom of Replacement. Typically, ph defines a function from x to y . (Contributed by NM, 26-Nov-1995)

	Ref	Expression
Hypotheses	zfrepclf.1	⊢ Ⅎ 𝑥 𝐴
	zfrepclf.2	⊢ 𝐴 ∈ V
	zfrepclf.3	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
Assertion	zfrepclf	⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		zfrepclf.1	⊢ Ⅎ 𝑥 𝐴
2		zfrepclf.2	⊢ 𝐴 ∈ V
3		zfrepclf.3	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) )
4	1	nfeq2	⊢ Ⅎ 𝑥 𝑣 = 𝐴
5		eleq2	⊢ ( 𝑣 = 𝐴 → ( 𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝐴 ) )
6	5 3	biimtrdi	⊢ ( 𝑣 = 𝐴 → ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) )
7	4 6	alrimi	⊢ ( 𝑣 = 𝐴 → ∀ 𝑥 ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) )
8		nfv	⊢ Ⅎ 𝑧 𝜑
9	8	axrep5	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑣 → ∃ 𝑧 ∀ 𝑦 ( 𝜑 → 𝑦 = 𝑧 ) ) → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) )
10	7 9	syl	⊢ ( 𝑣 = 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) )
11	5	anbi1d	⊢ ( 𝑣 = 𝐴 → ( ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
12	4 11	exbid	⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
13	12	bibi2d	⊢ ( 𝑣 = 𝐴 → ( ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) ↔ ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
14	13	albidv	⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
15	14	exbidv	⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑣 ∧ 𝜑 ) ) ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) )
16	10 15	mpbid	⊢ ( 𝑣 = 𝐴 → ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
17	2 16	vtocle	⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )