Theorem opex 4230

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 4229	. 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 2738   <.cop 3596

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 4122  ax-pow 4175  ax-pr 4210

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 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602

This theorem is referenced by:  otth2  4242  opabid  4258  elopab  4259  opabm  4281  elvvv  4690  relsnop  4733  xpiindim  4765  raliunxp  4769  rexiunxp  4770  intirr  5016  xpmlem  5050  dmsnm  5095  dmsnopg  5101  cnvcnvsn  5106  op2ndb  5113  cnviinm  5171  funopg  5251  fsn  5689  fvsn  5712  idref  5758  oprabid  5907  dfoprab2  5922  rnoprab  5958  fo1st  6158  fo2nd  6159  eloprabi  6197  xporderlem  6232  cnvoprab  6235  dmtpos  6257  rntpos  6258  tpostpos  6265  iinerm  6607  th3qlem2  6638  elixpsn  6735  ensn1  6796  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpassen  6830  xpmapenlem  6849  phplem2  6853  ac6sfi  6898  djuss  7069  genipdm  7515  ioof  9971  fsumcnv  11445  fprodcnv  11633  prdsex  12718  txdis1cn  13781