ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opex Structured version   GIF version

Theorem opex 3939
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 V
opex.2 B V
Assertion
Ref Expression
opex A, B V

Proof of Theorem opex
StepHypRef Expression
1 opex.1 . 2 A V
2 opex.2 . 2 B V
3 opexg 3937 . 2 ((A V B V) → ⟨A, B V)
41, 2, 3mp2an 404 1 A, B V
Colors of variables: wff set class
Syntax hints:   wcel 1375  Vcvv 2534  cop 3352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005  ax-sep 3848  ax-pow 3900  ax-pr 3917
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-v 2536  df-un 2898  df-in 2900  df-ss 2907  df-pw 3335  df-sn 3355  df-pr 3356  df-op 3358
This theorem is referenced by:  opabid  3967  elopab  3968  opabm  3990  elvvv  4328  xpiindim  4398  raliunxp  4402  rexiunxp  4403  intirr  4636  xpmlem  4669  dmsnm  4711  dmsnopg  4717  cnvcnvsn  4722  cnviinm  4784  funopg  4858  fsn  5258  idref  5319  oprabid  5459  dfoprab2  5473  rnoprab  5508  fo1st  5704  fo2nd  5705  eloprabi  5742  xporderlem  5771  dmtpos  5790  rntpos  5791  tpostpos  5798  tfrlemi14  5864  iinerm  6082  th3qlem2  6113  genipdm  6349  genpelpw  6350
  Copyright terms: Public domain W3C validator