Metamath Proof Explorer


Theorem opelopabt

Description: Closed theorem form of opelopab . (Contributed by NM, 19-Feb-2013)

Ref Expression
Assertion opelopabt ( ( ∀ 𝑥𝑦 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥𝑦 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ∧ ( 𝐴𝑉𝐵𝑊 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 elopab ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2 19.26-2 ( ∀ 𝑥𝑦 ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ) ↔ ( ∀ 𝑥𝑦 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥𝑦 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ) )
3 anim12 ( ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ) → ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( ( 𝜑𝜓 ) ∧ ( 𝜓𝜒 ) ) ) )
4 bitr ( ( ( 𝜑𝜓 ) ∧ ( 𝜓𝜒 ) ) → ( 𝜑𝜒 ) )
5 3 4 syl6 ( ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ) → ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜒 ) ) )
6 5 2alimi ( ∀ 𝑥𝑦 ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ) → ∀ 𝑥𝑦 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜒 ) ) )
7 2 6 sylbir ( ( ∀ 𝑥𝑦 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥𝑦 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ) → ∀ 𝑥𝑦 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜒 ) ) )
8 copsex2t ( ( ∀ 𝑥𝑦 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝜑𝜒 ) ) ∧ ( 𝐴𝑉𝐵𝑊 ) ) → ( ∃ 𝑥𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜒 ) )
9 7 8 stoic3 ( ( ∀ 𝑥𝑦 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥𝑦 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ∧ ( 𝐴𝑉𝐵𝑊 ) ) → ( ∃ 𝑥𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜒 ) )
10 1 9 syl5bb ( ( ∀ 𝑥𝑦 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ∧ ∀ 𝑥𝑦 ( 𝑦 = 𝐵 → ( 𝜓𝜒 ) ) ∧ ( 𝐴𝑉𝐵𝑊 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )