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

Theorem opexg 3937
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 11-Jan-2019.)
Assertion
Ref Expression
opexg ((A 𝑉 B 𝑊) → ⟨A, B V)

Proof of Theorem opexg
StepHypRef Expression
1 dfopg 3520 . 2 ((A 𝑉 B 𝑊) → ⟨A, B⟩ = {{A}, {A, B}})
2 elex 2542 . . . . 5 (A 𝑉A V)
3 snexg 3909 . . . . 5 (A V → {A} V)
42, 3syl 14 . . . 4 (A 𝑉 → {A} V)
54adantr 261 . . 3 ((A 𝑉 B 𝑊) → {A} V)
6 elex 2542 . . . 4 (B 𝑊B V)
7 prexg 3920 . . . 4 ((A V B V) → {A, B} V)
82, 6, 7syl2an 273 . . 3 ((A 𝑉 B 𝑊) → {A, B} V)
9 prexg 3920 . . 3 (({A} V {A, B} V) → {{A}, {A, B}} V)
105, 8, 9syl2anc 393 . 2 ((A 𝑉 B 𝑊) → {{A}, {A, B}} V)
111, 10eqeltrd 2097 1 ((A 𝑉 B 𝑊) → ⟨A, B V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1375  Vcvv 2534  {csn 3349  {cpr 3350  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:  opex  3939  otexg  3940  fliftel1  5357  oprabid  5459  eloprabga  5512  op1st  5693  op2nd  5694  ot1stg  5699  ot2ndg  5700  ot3rdgg  5701  elxp6  5716  mpt2fvex  5749  algrflem  5770  mpt2xopoveq  5774  brtposg  5788  tfrlemisucaccv  5855  tfrlemibxssdm  5857  tfrlemibfn  5858  tfrlemi14d  5863  mulpipq2  6222  enq0breq  6277
  Copyright terms: Public domain W3C validator