Theorem bj-dfres2

Description: Alternate definition of the restriction of a class to another, as an ordered pair class abstraction: the restriction of a class to another is the class of ordered pairs whose first component is in the restricting class and whose components are related by the restricted class. (Contributed by Mario Carneiro, 5-Nov-2013) Do not depend on df-rel . (Revised by BJ, 16-Oct-2026)

	Ref	Expression
Assertion	bj-dfres2	⊢ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
2		an12	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
3	2	exbii	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
4		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) )
5	3 4	bitr2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
6	5	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
7	1 6	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
8		bj-elres	⊢ ( 𝑧 ∈ ( 𝑅 ↾ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝑅 𝑦 ) )
9		elopab	⊢ ( 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
10	7 8 9	3bitr4i	⊢ ( 𝑧 ∈ ( 𝑅 ↾ 𝐴 ) ↔ 𝑧 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) } )
11	10	eqriv	⊢ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑦 ) }