Theorem dropab2

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	dropab2	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { ⟨ 𝑧 , 𝑥 ⟩ ∣ 𝜑 } = { ⟨ 𝑧 , 𝑦 ⟩ ∣ 𝜑 } )

Proof

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