Theorem zfrep4

Description: A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995)

	Ref	Expression
Hypotheses	zfrep4.1	⊢ { 𝑥 ∣ 𝜑 } ∈ V
	zfrep4.2	⊢ ( 𝜑 → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
Assertion	zfrep4	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) } ∈ V

Proof

Step	Hyp	Ref	Expression
1		zfrep4.1	⊢ { 𝑥 ∣ 𝜑 } ∈ V
2		zfrep4.2	⊢ ( 𝜑 → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
3		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
4	3	anbi1i	⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜓 ) )
5	4	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ↔ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
6	5	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } = { 𝑦 ∣ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) }
7		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
8	3 2	sylbi	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } → ∃ 𝑧 ∀ 𝑦 ( 𝜓 → 𝑦 = 𝑧 ) )
9	7 1 8	zfrepclf	⊢ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) )
10		abeq2	⊢ ( 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ) )
11	10	exbii	⊢ ( ∃ 𝑧 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } ↔ ∃ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) ) )
12	9 11	mpbir	⊢ ∃ 𝑧 𝑧 = { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) }
13	12	issetri	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ 𝜓 ) } ∈ V
14	6 13	eqeltrri	⊢ { 𝑦 ∣ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) } ∈ V