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

Metamath Proof Explorer

Theorem opabbrex

Description: A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by BJ/AV, 20-Jun-2019) (Proof shortened by OpenAI, 25-Mar-2020)

		Ref	Expression
	Assertion	opabbrex	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝜑 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝜑 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ 𝑉 )
2		pm3.41	⊢ ( ( 𝑥 𝑅 𝑦 → 𝜑 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) → 𝜑 ) )
3	2	2alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) → 𝜑 ) )
4	3	adantr	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝜑 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ 𝑉 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) → 𝜑 ) )
5		ssopab2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) → 𝜑 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
6	4 5	syl	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝜑 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
7	1 6	ssexd	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝜑 ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∈ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 𝑅 𝑦 ∧ 𝜓 ) } ∈ V )