Theorem eloprabi

Description: A consequence of membership in an operation class abstraction, using ordered pair extractors. (Contributed by NM, 6-Nov-2006) (Revised by David Abernethy, 19-Jun-2012)

	Ref	Expression
Hypotheses	eloprabi.1	⊢ ( 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜑 ↔ 𝜓 ) )
	eloprabi.2	⊢ ( 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜓 ↔ 𝜒 ) )
	eloprabi.3	⊢ ( 𝑧 = ( 2nd ‘ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) )
Assertion	eloprabi	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		eloprabi.1	⊢ ( 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜑 ↔ 𝜓 ) )
2		eloprabi.2	⊢ ( 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) → ( 𝜓 ↔ 𝜒 ) )
3		eloprabi.3	⊢ ( 𝑧 = ( 2nd ‘ 𝐴 ) → ( 𝜒 ↔ 𝜃 ) )
4		eqeq1	⊢ ( 𝑤 = 𝐴 → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5	4	anbi1d	⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
6	5	3exbidv	⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
7		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
8	6 7	elab2g	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
9	8	ibi	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
10		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
11		vex	⊢ 𝑧 ∈ V
12	10 11	op1std	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1st ‘ 𝐴 ) = ⟨ 𝑥 , 𝑦 ⟩ )
13	12	fveq2d	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1st ‘ ( 1st ‘ 𝐴 ) ) = ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
14		vex	⊢ 𝑥 ∈ V
15		vex	⊢ 𝑦 ∈ V
16	14 15	op1st	⊢ ( 1st ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑥
17	13 16	eqtr2di	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑥 = ( 1st ‘ ( 1st ‘ 𝐴 ) ) )
18	17 1	syl	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜓 ) )
19	12	fveq2d	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2nd ‘ ( 1st ‘ 𝐴 ) ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
20	14 15	op2nd	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
21	19 20	eqtr2di	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑦 = ( 2nd ‘ ( 1st ‘ 𝐴 ) ) )
22	21 2	syl	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜓 ↔ 𝜒 ) )
23	10 11	op2ndd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑧 )
24	23	eqcomd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑧 = ( 2nd ‘ 𝐴 ) )
25	24 3	syl	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜒 ↔ 𝜃 ) )
26	18 22 25	3bitrd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜃 ) )
27	26	biimpa	⊢ ( ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
28	27	exlimiv	⊢ ( ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
29	28	exlimiv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
30	29	exlimiv	⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜃 )
31	9 30	syl	⊢ ( 𝐴 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → 𝜃 )