Theorem opex 4274

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 4273	. 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 2176   _Vcvv 2772   <.cop 3636

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  otth2  4286  opabid  4303  elopab  4305  opabm  4328  elvvv  4739  relsnop  4782  xpiindim  4816  raliunxp  4820  rexiunxp  4821  intirr  5070  xpmlem  5104  dmsnm  5149  dmsnopg  5155  cnvcnvsn  5160  op2ndb  5167  cnviinm  5225  funopg  5306  fsn  5754  fvsn  5781  idref  5827  oprabid  5978  dfoprab2  5994  rnoprab  6030  fo1st  6245  fo2nd  6246  eloprabi  6284  xporderlem  6319  cnvoprab  6322  dmtpos  6344  rntpos  6345  tpostpos  6352  iinerm  6696  th3qlem2  6727  elixpsn  6824  ensn1  6890  mapsnen  6905  xpsnen  6918  xpcomco  6923  xpassen  6927  xpmapenlem  6948  phplem2  6952  ac6sfi  6997  djuss  7174  genipdm  7631  ioof  10095  wrdexb  11008  fsumcnv  11781  fprodcnv  11969  nninfct  12395  prdsex  13134  fnpsr  14462  txdis1cn  14783