Metamath Proof Explorer


Theorem eliminable-abelab

Description: A theorem used to prove the base case of the Eliminability Theorem (see section comment): abstraction belongs to abstraction. (Contributed by BJ, 30-Apr-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion eliminable-abelab ( { 𝑥𝜑 } ∈ { 𝑦𝜓 } ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 dfclel ( { 𝑥𝜑 } ∈ { 𝑦𝜓 } ↔ ∃ 𝑧 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 ∈ { 𝑦𝜓 } ) )
2 eliminable-veqab ( 𝑧 = { 𝑥𝜑 } ↔ ∀ 𝑡 ( 𝑡𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) )
3 eliminable-velab ( 𝑧 ∈ { 𝑦𝜓 } ↔ [ 𝑧 / 𝑦 ] 𝜓 )
4 2 3 anbi12i ( ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 ∈ { 𝑦𝜓 } ) ↔ ( ∀ 𝑡 ( 𝑡𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) )
5 4 exbii ( ∃ 𝑧 ( 𝑧 = { 𝑥𝜑 } ∧ 𝑧 ∈ { 𝑦𝜓 } ) ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) )
6 1 5 bitri ( { 𝑥𝜑 } ∈ { 𝑦𝜓 } ↔ ∃ 𝑧 ( ∀ 𝑡 ( 𝑡𝑧 ↔ [ 𝑡 / 𝑥 ] 𝜑 ) ∧ [ 𝑧 / 𝑦 ] 𝜓 ) )