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

Metamath Proof Explorer

Theorem dfopg

Description: Value of the ordered pair when the arguments are sets. (Contributed by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

Ref Expression
Assertion dfopg ⊢ A ∈ V ∧ B ∈ W → A B = A A B

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ V → A ∈ V
2 elex ⊢ B ∈ W → B ∈ V
3 dfopif ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅
4 iftrue ⊢ A ∈ V ∧ B ∈ V → if A ∈ V ∧ B ∈ V A A B ∅ = A A B
5 3 4 eqtrid ⊢ A ∈ V ∧ B ∈ V → A B = A A B
6 1 2 5 syl2an ⊢ A ∈ V ∧ B ∈ W → A B = A A B