Theorem opex 3939

Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)

Hypotheses

Ref	Expression
opex.1	⊢ A ∈ V
opex.2	⊢ B ∈ V

Assertion

Ref	Expression
opex	⊢ ⟨A, B⟩ ∈ V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		opex.1	. 2 ⊢ A ∈ V
2		opex.2	. 2 ⊢ B ∈ V
3		opexg 3937	. 2 ⊢ ((A ∈ V ∧ B ∈ V) → ⟨A, B⟩ ∈ V)
4	1, 2, 3	mp2an 404	1 ⊢ ⟨A, B⟩ ∈ V

Syntax hints:   ∈ wcel 1375  Vcvv 2534  ⟨cop 3352

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005  ax-sep 3848  ax-pow 3900  ax-pr 3917

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-v 2536  df-un 2898  df-in 2900  df-ss 2907  df-pw 3335  df-sn 3355  df-pr 3356  df-op 3358

This theorem is referenced by:  opabid  3967  elopab  3968  opabm  3990  elvvv  4328  xpiindim  4398  raliunxp  4402  rexiunxp  4403  intirr  4636  xpmlem  4669  dmsnm  4711  dmsnopg  4717  cnvcnvsn  4722  cnviinm  4784  funopg  4858  fsn  5258  idref  5319  oprabid  5459  dfoprab2  5473  rnoprab  5508  fo1st  5704  fo2nd  5705  eloprabi  5742  xporderlem  5771  dmtpos  5790  rntpos  5791  tpostpos  5798  tfrlemi14  5864  iinerm  6082  th3qlem2  6113  genipdm  6349  genpelpw  6350