Theorem opex 4319

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 4318	. 2 |- ( ( A e. _V /\ B e. _V ) -> <. A , B >. e. _V )
4	1, 2, 3	mp2an 426	1 |- <. A , B >. e. _V

Syntax hints:   e. wcel 2200   _Vcvv 2800   <.cop 3670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676

This theorem is referenced by:  otth2  4331  opabid  4348  elopab  4350  opabm  4373  elvvv  4787  relsnop  4830  xpiindim  4865  raliunxp  4869  rexiunxp  4870  intirr  5121  xpmlem  5155  dmsnm  5200  dmsnopg  5206  cnvcnvsn  5211  op2ndb  5218  cnviinm  5276  funopg  5358  fsn  5815  fvsn  5844  idref  5892  oprabid  6045  dfoprab2  6063  rnoprab  6099  fo1st  6315  fo2nd  6316  eloprabi  6356  xporderlem  6391  cnvoprab  6394  dmtpos  6417  rntpos  6418  tpostpos  6425  iinerm  6771  th3qlem2  6802  elixpsn  6899  ensn1  6965  mapsnen  6981  dom1o  6997  xpsnen  7000  xpcomco  7005  xpassen  7009  xpmapenlem  7030  phplem2  7034  ac6sfi  7080  djuss  7260  genipdm  7726  ioof  10196  wrdexb  11115  fsumcnv  11988  fprodcnv  12176  nninfct  12602  prdsex  13342  fnpsr  14671  txdis1cn  14992  griedg0ssusgr  16090