Theorem inopab

Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

	Ref	Expression
Assertion	inopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		relopab	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		relin1	⊢ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
3	1 2	ax-mp	⊢ Rel ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } )
4		relopab	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }
5		sban	⊢ ( [ 𝑤 / 𝑦 ] ( [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜓 ) )
6		sban	⊢ ( [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) )
7	6	sbbii	⊢ ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑤 / 𝑦 ] ( [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑧 / 𝑥 ] 𝜓 ) )
8		opelopabsbALT	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
9		opelopabsbALT	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜓 )
10	8 9	anbi12i	⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ∧ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜓 ) )
11	5 7 10	3bitr4ri	⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) )
12		elin	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) )
13		opelopabsbALT	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) )
14	11 12 13	3bitr4i	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ ∈ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) ↔ ⟨ 𝑧 , 𝑤 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) } )
15	3 4 14	eqrelriiv	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∩ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝜓 ) }