Theorem opex 4345

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 4344	. 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 2203   _Vcvv 2813   <.cop 3692

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698

This theorem is referenced by:  otth2  4357  opabid  4374  elopab  4376  opabm  4399  elvvv  4813  relsnop  4856  xpiindim  4892  raliunxp  4896  rexiunxp  4897  intirr  5149  xpmlem  5183  dmsnm  5228  dmsnopg  5234  cnvcnvsn  5239  op2ndb  5246  cnviinm  5304  funopg  5386  fsn  5849  fvsn  5879  idref  5929  oprabid  6082  dfoprab2  6100  rnoprab  6136  fo1st  6351  fo2nd  6352  eloprabi  6392  xporderlem  6427  cnvoprab  6430  dmtpos  6487  rntpos  6488  tpostpos  6495  iinerm  6841  th3qlem2  6872  elixpsn  6970  ensn1  7036  mapsnen  7053  dom1o  7069  xpsnen  7072  xpcomco  7077  xpassen  7081  xpmapenlem  7102  phplem2  7107  ac6sfi  7155  djuss  7361  genipdm  7831  ioof  10304  wrdexb  11236  fsumcnv  12123  fprodcnv  12311  nninfct  12737  prdsex  13482  fnpsr  14815  txdis1cn  15143  griedg0ssusgr  16246