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

Metamath Proof Explorer

Theorem dfop

Description: Value of an ordered pair when the arguments are sets, with the conclusion corresponding to Kuratowski's original definition. (Contributed by NM, 25-Jun-1998) (Avoid depending on this detail.)

Ref Expression
Hypotheses dfop.1 ⊢ A ∈ V
dfop.2 ⊢ B ∈ V
Assertion dfop ⊢ A B = A A B

Proof

Step Hyp Ref Expression
1 dfop.1 ⊢ A ∈ V
2 dfop.2 ⊢ B ∈ V
3 dfopg ⊢ A ∈ V ∧ B ∈ V → A B = A A B
4 1 2 3 mp2an ⊢ A B = A A B