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

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

Proof of Theorem opexg
StepHypRef Expression
1 dfopg 3544 . 2 ((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ = {{𝐴}, {𝐴, 𝐵}})
2 elex 2563 . . . . 5 (𝐴𝑉𝐴 ∈ V)
3 snexg 3933 . . . . 5 (𝐴 ∈ V → {𝐴} ∈ V)
42, 3syl 14 . . . 4 (𝐴𝑉 → {𝐴} ∈ V)
54adantr 261 . . 3 ((𝐴𝑉𝐵𝑊) → {𝐴} ∈ V)
6 elex 2563 . . . 4 (𝐵𝑊𝐵 ∈ V)
7 prexg 3944 . . . 4 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
82, 6, 7syl2an 273 . . 3 ((𝐴𝑉𝐵𝑊) → {𝐴, 𝐵} ∈ V)
9 prexg 3944 . . 3 (({𝐴} ∈ V ∧ {𝐴, 𝐵} ∈ V) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
105, 8, 9syl2anc 391 . 2 ((𝐴𝑉𝐵𝑊) → {{𝐴}, {𝐴, 𝐵}} ∈ V)
111, 10eqeltrd 2114 1 ((𝐴𝑉𝐵𝑊) → ⟨𝐴, 𝐵⟩ ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  Vcvv 2554  {csn 3372  {cpr 3373  cop 3375
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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3872  ax-pow 3924  ax-pr 3941
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381
This theorem is referenced by:  opex  3963  otexg  3964  fliftel1  5421  oprabid  5524  ovexg  5526  eloprabga  5578  op1st  5760  op2nd  5761  ot1stg  5766  ot2ndg  5767  ot3rdgg  5768  elxp6  5783  mpt2fvex  5816  algrflem  5837  algrflemg  5838  mpt2xopoveq  5842  brtposg  5856  tfr0  5924  tfrlemisucaccv  5926  tfrlemibxssdm  5928  tfrlemibfn  5929  tfrlemi14d  5934  mulpipq2  6450  enq0breq  6515  addvalex  6901  peano2nnnn  6910  axcnre  6936  frec2uzrdg  9073  frecuzrdg0  9078  frecuzrdgsuc  9079
  Copyright terms: Public domain W3C validator