Theorem dropab1

Description: Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	dropab1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑧 ⟩ )
2	1	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑧 ⟩ )
3	2	eqeq2d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ) )
4	3	anbi1d	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
5	4	drex2	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
6	5	drex1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
7	6	abbidv	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝜑 ) } = { 𝑤 ∣ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) } )
8		df-opab	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝜑 ) }
9		df-opab	⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) }
10	7 8 9	3eqtr4g	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )