Theorem oprabrexex2

Description: Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

	Ref	Expression
Hypotheses	oprabrexex2.1	⊢ 𝐴 ∈ V
	oprabrexex2.2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ∈ V
Assertion	oprabrexex2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤 ∈ 𝐴 𝜑 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		oprabrexex2.1	⊢ 𝐴 ∈ V
2		oprabrexex2.2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ∈ V
3		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤 ∈ 𝐴 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) }
4		rexcom4	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
5		rexcom4	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
6		rexcom4	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∈ 𝐴 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
7		r19.42v	⊢ ( ∃ 𝑤 ∈ 𝐴 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) )
8	7	exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ∈ 𝐴 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) )
9	6 8	bitri	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) )
10	9	exbii	⊢ ( ∃ 𝑦 ∃ 𝑤 ∈ 𝐴 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) )
11	5 10	bitri	⊢ ( ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) )
12	11	exbii	⊢ ( ∃ 𝑥 ∃ 𝑤 ∈ 𝐴 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) )
13	4 12	bitr2i	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) ↔ ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
14	13	abbii	⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ∃ 𝑤 ∈ 𝐴 𝜑 ) } = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
15	3 14	eqtri	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤 ∈ 𝐴 𝜑 } = { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
16		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
17	16 2	eqeltrri	⊢ { 𝑣 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } ∈ V
18	1 17	abrexex2	⊢ { 𝑣 ∣ ∃ 𝑤 ∈ 𝐴 ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } ∈ V
19	15 18	eqeltri	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑤 ∈ 𝐴 𝜑 } ∈ V