Theorem opex 4278

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 4277	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ ∈ V)
4	1, 2, 3	mp2an 426	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∈ wcel 2177  Vcvv 2773  ⟨cop 3638

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644

This theorem is referenced by:  otth2  4290  opabid  4307  elopab  4309  opabm  4332  elvvv  4743  relsnop  4786  xpiindim  4820  raliunxp  4824  rexiunxp  4825  intirr  5075  xpmlem  5109  dmsnm  5154  dmsnopg  5160  cnvcnvsn  5165  op2ndb  5172  cnviinm  5230  funopg  5311  fsn  5762  fvsn  5789  idref  5835  oprabid  5986  dfoprab2  6002  rnoprab  6038  fo1st  6253  fo2nd  6254  eloprabi  6292  xporderlem  6327  cnvoprab  6330  dmtpos  6352  rntpos  6353  tpostpos  6360  iinerm  6704  th3qlem2  6735  elixpsn  6832  ensn1  6898  mapsnen  6914  xpsnen  6928  xpcomco  6933  xpassen  6937  xpmapenlem  6958  phplem2  6962  ac6sfi  7007  djuss  7184  genipdm  7642  ioof  10106  wrdexb  11019  fsumcnv  11798  fprodcnv  11986  nninfct  12412  prdsex  13151  fnpsr  14479  txdis1cn  14800  dom1o  16043