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

Theorem opabex3d 5687
Description: Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017.)
Hypotheses
Ref Expression
opabex3d.1 (φA V)
opabex3d.2 ((φ x A) → {yψ} V)
Assertion
Ref Expression
opabex3d (φ → {⟨x, y⟩ ∣ (x A ψ)} V)
Distinct variable groups:   x,A,y   φ,x
Allowed substitution hints:   φ(y)   ψ(x,y)

Proof of Theorem opabex3d
Dummy variables v w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.42v 1783 . . . . . 6 (y(x A (z = ⟨x, y ψ)) ↔ (x A y(z = ⟨x, y ψ)))
2 an12 495 . . . . . . 7 ((z = ⟨x, y (x A ψ)) ↔ (x A (z = ⟨x, y ψ)))
32exbii 1493 . . . . . 6 (y(z = ⟨x, y (x A ψ)) ↔ y(x A (z = ⟨x, y ψ)))
4 elxp 4304 . . . . . . . 8 (z ({x} × {yψ}) ↔ vw(z = ⟨v, w (v {x} w {yψ})))
5 excom 1551 . . . . . . . . 9 (vw(z = ⟨v, w (v {x} w {yψ})) ↔ wv(z = ⟨v, w (v {x} w {yψ})))
6 an12 495 . . . . . . . . . . . . 13 ((z = ⟨v, w (v {x} w {yψ})) ↔ (v {x} (z = ⟨v, w w {yψ})))
7 elsn 3381 . . . . . . . . . . . . . 14 (v {x} ↔ v = x)
87anbi1i 431 . . . . . . . . . . . . 13 ((v {x} (z = ⟨v, w w {yψ})) ↔ (v = x (z = ⟨v, w w {yψ})))
96, 8bitri 173 . . . . . . . . . . . 12 ((z = ⟨v, w (v {x} w {yψ})) ↔ (v = x (z = ⟨v, w w {yψ})))
109exbii 1493 . . . . . . . . . . 11 (v(z = ⟨v, w (v {x} w {yψ})) ↔ v(v = x (z = ⟨v, w w {yψ})))
11 vex 2554 . . . . . . . . . . . 12 x V
12 opeq1 3539 . . . . . . . . . . . . . 14 (v = x → ⟨v, w⟩ = ⟨x, w⟩)
1312eqeq2d 2048 . . . . . . . . . . . . 13 (v = x → (z = ⟨v, w⟩ ↔ z = ⟨x, w⟩))
1413anbi1d 438 . . . . . . . . . . . 12 (v = x → ((z = ⟨v, w w {yψ}) ↔ (z = ⟨x, w w {yψ})))
1511, 14ceqsexv 2587 . . . . . . . . . . 11 (v(v = x (z = ⟨v, w w {yψ})) ↔ (z = ⟨x, w w {yψ}))
1610, 15bitri 173 . . . . . . . . . 10 (v(z = ⟨v, w (v {x} w {yψ})) ↔ (z = ⟨x, w w {yψ}))
1716exbii 1493 . . . . . . . . 9 (wv(z = ⟨v, w (v {x} w {yψ})) ↔ w(z = ⟨x, w w {yψ}))
185, 17bitri 173 . . . . . . . 8 (vw(z = ⟨v, w (v {x} w {yψ})) ↔ w(z = ⟨x, w w {yψ}))
19 nfv 1418 . . . . . . . . . 10 y z = ⟨x, w
20 nfsab1 2027 . . . . . . . . . 10 y w {yψ}
2119, 20nfan 1454 . . . . . . . . 9 y(z = ⟨x, w w {yψ})
22 nfv 1418 . . . . . . . . 9 w(z = ⟨x, y ψ)
23 opeq2 3540 . . . . . . . . . . 11 (w = y → ⟨x, w⟩ = ⟨x, y⟩)
2423eqeq2d 2048 . . . . . . . . . 10 (w = y → (z = ⟨x, w⟩ ↔ z = ⟨x, y⟩))
25 sbequ12 1651 . . . . . . . . . . . 12 (y = w → (ψ ↔ [w / y]ψ))
2625equcoms 1591 . . . . . . . . . . 11 (w = y → (ψ ↔ [w / y]ψ))
27 df-clab 2024 . . . . . . . . . . 11 (w {yψ} ↔ [w / y]ψ)
2826, 27syl6rbbr 188 . . . . . . . . . 10 (w = y → (w {yψ} ↔ ψ))
2924, 28anbi12d 442 . . . . . . . . 9 (w = y → ((z = ⟨x, w w {yψ}) ↔ (z = ⟨x, y ψ)))
3021, 22, 29cbvex 1636 . . . . . . . 8 (w(z = ⟨x, w w {yψ}) ↔ y(z = ⟨x, y ψ))
314, 18, 303bitri 195 . . . . . . 7 (z ({x} × {yψ}) ↔ y(z = ⟨x, y ψ))
3231anbi2i 430 . . . . . 6 ((x A z ({x} × {yψ})) ↔ (x A y(z = ⟨x, y ψ)))
331, 3, 323bitr4ri 202 . . . . 5 ((x A z ({x} × {yψ})) ↔ y(z = ⟨x, y (x A ψ)))
3433exbii 1493 . . . 4 (x(x A z ({x} × {yψ})) ↔ xy(z = ⟨x, y (x A ψ)))
35 eliun 3651 . . . . 5 (z x A ({x} × {yψ}) ↔ x A z ({x} × {yψ}))
36 df-rex 2306 . . . . 5 (x A z ({x} × {yψ}) ↔ x(x A z ({x} × {yψ})))
3735, 36bitri 173 . . . 4 (z x A ({x} × {yψ}) ↔ x(x A z ({x} × {yψ})))
38 elopab 3985 . . . 4 (z {⟨x, y⟩ ∣ (x A ψ)} ↔ xy(z = ⟨x, y (x A ψ)))
3934, 37, 383bitr4i 201 . . 3 (z x A ({x} × {yψ}) ↔ z {⟨x, y⟩ ∣ (x A ψ)})
4039eqriv 2034 . 2 x A ({x} × {yψ}) = {⟨x, y⟩ ∣ (x A ψ)}
41 opabex3d.1 . . 3 (φA V)
42 snexg 3926 . . . . . 6 (x V → {x} V)
4311, 42ax-mp 7 . . . . 5 {x} V
44 opabex3d.2 . . . . 5 ((φ x A) → {yψ} V)
45 xpexg 4394 . . . . 5 (({x} V {yψ} V) → ({x} × {yψ}) V)
4643, 44, 45sylancr 393 . . . 4 ((φ x A) → ({x} × {yψ}) V)
4746ralrimiva 2386 . . 3 (φx A ({x} × {yψ}) V)
48 iunexg 5685 . . 3 ((A V x A ({x} × {yψ}) V) → x A ({x} × {yψ}) V)
4941, 47, 48syl2anc 391 . 2 (φ x A ({x} × {yψ}) V)
5040, 49syl5eqelr 2122 1 (φ → {⟨x, y⟩ ∣ (x A ψ)} V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242  wex 1378   wcel 1390  [wsb 1642  {cab 2023  wral 2300  wrex 2301  Vcvv 2551  {csn 3366  cop 3369   ciun 3647  {copab 3807   × cxp 4285
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3862  ax-sep 3865  ax-pow 3917  ax-pr 3934  ax-un 4135
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3352  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-iun 3649  df-br 3755  df-opab 3809  df-mpt 3810  df-id 4020  df-xp 4293  df-rel 4294  df-cnv 4295  df-co 4296  df-dm 4297  df-rn 4298  df-res 4299  df-ima 4300  df-iota 4809  df-fun 4846  df-fn 4847  df-f 4848  df-f1 4849  df-fo 4850  df-f1o 4851  df-fv 4852
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator