This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssoprab2

Description: Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2 . (Contributed by FL, 6-Nov-2013) (Proof shortened by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion ssoprab2 ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } )

Proof

Step Hyp Ref Expression
1 id ⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜓 ) )
2 1 anim2d ⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜓 ) ) )
3 2 aleximi ⊢ ( ∀ 𝑧 ( 𝜑 → 𝜓 ) → ( ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜓 ) ) )
4 3 aleximi ⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) → ( ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜓 ) ) )
5 4 aleximi ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜓 ) ) )
6 5 ss2abdv ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) → { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) } ⊆ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜓 ) } )
7 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
8 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜓 ) }
9 6 7 8 3sstr4g ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( 𝜑 → 𝜓 ) → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ⊆ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜓 } )