Theorem opex 4067

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 e. _V
opex.2	|- B e. _V

Assertion

Ref	Expression
opex	|- <. A , B >. e. _V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		opex.1	. 2 |- A e. _V
2		opex.2	. 2 |- B e. _V
3		opexg 4066	. 2 |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. e. _V )
4	1, 2, 3	mp2an 418	1 |- <. A , B >. e. _V

Syntax hints:   e. wcel 1439   _Vcvv 2622   <.cop 3455

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2624  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461

This theorem is referenced by:  otth2  4079  opabid  4095  elopab  4096  opabm  4118  elvvv  4516  relsnop  4559  xpiindim  4588  raliunxp  4592  rexiunxp  4593  intirr  4833  xpmlem  4867  dmsnm  4911  dmsnopg  4917  cnvcnvsn  4922  op2ndb  4929  cnviinm  4987  funopg  5063  fsn  5485  fvsn  5508  idref  5552  oprabid  5697  dfoprab2  5712  rnoprab  5747  fo1st  5944  fo2nd  5945  eloprabi  5982  xporderlem  6012  cnvoprab  6015  dmtpos  6037  rntpos  6038  tpostpos  6045  iinerm  6380  th3qlem2  6411  elixpsn  6508  ensn1  6569  mapsnen  6584  xpsnen  6593  xpcomco  6598  xpassen  6602  xpmapenlem  6621  phplem2  6625  ac6sfi  6670  djuss  6817  genipdm  7138  ioof  9452  fsumcnv  10894