Theorem opex 4229

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 4228	. 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 2148   _Vcvv 2737   <.cop 3595

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601

This theorem is referenced by:  otth2  4241  opabid  4257  elopab  4258  opabm  4280  elvvv  4689  relsnop  4732  xpiindim  4764  raliunxp  4768  rexiunxp  4769  intirr  5015  xpmlem  5049  dmsnm  5094  dmsnopg  5100  cnvcnvsn  5105  op2ndb  5112  cnviinm  5170  funopg  5250  fsn  5688  fvsn  5711  idref  5757  oprabid  5906  dfoprab2  5921  rnoprab  5957  fo1st  6157  fo2nd  6158  eloprabi  6196  xporderlem  6231  cnvoprab  6234  dmtpos  6256  rntpos  6257  tpostpos  6264  iinerm  6606  th3qlem2  6637  elixpsn  6734  ensn1  6795  mapsnen  6810  xpsnen  6820  xpcomco  6825  xpassen  6829  xpmapenlem  6848  phplem2  6852  ac6sfi  6897  djuss  7068  genipdm  7514  ioof  9970  fsumcnv  11444  fprodcnv  11632  prdsex  12717  txdis1cn  13748