Theorem opex 4314

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	⊢ 𝐴 ∈ V
opex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
opex	⊢ ⟨𝐴, 𝐵⟩ ∈ V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		opex.1	. 2 ⊢ 𝐴 ∈ V
2		opex.2	. 2 ⊢ 𝐵 ∈ V
3		opexg 4313	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ ∈ V)
4	1, 2, 3	mp2an 426	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∈ wcel 2200  Vcvv 2799  ⟨cop 3669

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 4201  ax-pow 4257  ax-pr 4292

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  otth2  4326  opabid  4343  elopab  4345  opabm  4368  elvvv  4779  relsnop  4822  xpiindim  4856  raliunxp  4860  rexiunxp  4861  intirr  5111  xpmlem  5145  dmsnm  5190  dmsnopg  5196  cnvcnvsn  5201  op2ndb  5208  cnviinm  5266  funopg  5348  fsn  5800  fvsn  5827  idref  5873  oprabid  6026  dfoprab2  6042  rnoprab  6078  fo1st  6293  fo2nd  6294  eloprabi  6332  xporderlem  6367  cnvoprab  6370  dmtpos  6392  rntpos  6393  tpostpos  6400  iinerm  6744  th3qlem2  6775  elixpsn  6872  ensn1  6938  mapsnen  6954  xpsnen  6968  xpcomco  6973  xpassen  6977  xpmapenlem  6998  phplem2  7002  ac6sfi  7048  djuss  7225  genipdm  7691  ioof  10155  wrdexb  11070  fsumcnv  11934  fprodcnv  12122  nninfct  12548  prdsex  13288  fnpsr  14616  txdis1cn  14937  dom1o  16286