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

Theorem dfoprab4f 5758
Description: Operation class abstraction expressed without existential quantifiers. (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Contributed by NM, 20-Dec-2008.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypotheses
Ref Expression
dfoprab4f.x xφ
dfoprab4f.y yφ
dfoprab4f.1 (w = ⟨x, y⟩ → (φψ))
Assertion
Ref Expression
dfoprab4f {⟨w, z⟩ ∣ (w (A × B) φ)} = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) ψ)}
Distinct variable groups:   x,w,y,z   w,A,x,y   w,B,x,y   ψ,w
Allowed substitution hints:   φ(x,y,z,w)   ψ(x,y,z)   A(z)   B(z)

Proof of Theorem dfoprab4f
Dummy variables u 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1418 . . . . 5 x w = ⟨𝑡, u
2 dfoprab4f.x . . . . . 6 xφ
3 nfs1v 1812 . . . . . 6 x[𝑡 / x][u / y]ψ
42, 3nfbi 1478 . . . . 5 x(φ ↔ [𝑡 / x][u / y]ψ)
51, 4nfim 1461 . . . 4 x(w = ⟨𝑡, u⟩ → (φ ↔ [𝑡 / x][u / y]ψ))
6 opeq1 3539 . . . . . 6 (x = 𝑡 → ⟨x, u⟩ = ⟨𝑡, u⟩)
76eqeq2d 2048 . . . . 5 (x = 𝑡 → (w = ⟨x, u⟩ ↔ w = ⟨𝑡, u⟩))
8 sbequ12 1651 . . . . . 6 (x = 𝑡 → ([u / y]ψ ↔ [𝑡 / x][u / y]ψ))
98bibi2d 221 . . . . 5 (x = 𝑡 → ((φ ↔ [u / y]ψ) ↔ (φ ↔ [𝑡 / x][u / y]ψ)))
107, 9imbi12d 223 . . . 4 (x = 𝑡 → ((w = ⟨x, u⟩ → (φ ↔ [u / y]ψ)) ↔ (w = ⟨𝑡, u⟩ → (φ ↔ [𝑡 / x][u / y]ψ))))
11 nfv 1418 . . . . . 6 y w = ⟨x, u
12 dfoprab4f.y . . . . . . 7 yφ
13 nfs1v 1812 . . . . . . 7 y[u / y]ψ
1412, 13nfbi 1478 . . . . . 6 y(φ ↔ [u / y]ψ)
1511, 14nfim 1461 . . . . 5 y(w = ⟨x, u⟩ → (φ ↔ [u / y]ψ))
16 opeq2 3540 . . . . . . 7 (y = u → ⟨x, y⟩ = ⟨x, u⟩)
1716eqeq2d 2048 . . . . . 6 (y = u → (w = ⟨x, y⟩ ↔ w = ⟨x, u⟩))
18 sbequ12 1651 . . . . . . 7 (y = u → (ψ ↔ [u / y]ψ))
1918bibi2d 221 . . . . . 6 (y = u → ((φψ) ↔ (φ ↔ [u / y]ψ)))
2017, 19imbi12d 223 . . . . 5 (y = u → ((w = ⟨x, y⟩ → (φψ)) ↔ (w = ⟨x, u⟩ → (φ ↔ [u / y]ψ))))
21 dfoprab4f.1 . . . . 5 (w = ⟨x, y⟩ → (φψ))
2215, 20, 21chvar 1637 . . . 4 (w = ⟨x, u⟩ → (φ ↔ [u / y]ψ))
235, 10, 22chvar 1637 . . 3 (w = ⟨𝑡, u⟩ → (φ ↔ [𝑡 / x][u / y]ψ))
2423dfoprab4 5757 . 2 {⟨w, z⟩ ∣ (w (A × B) φ)} = {⟨⟨𝑡, u⟩, z⟩ ∣ ((𝑡 A u B) [𝑡 / x][u / y]ψ)}
25 nfv 1418 . . 3 𝑡((x A y B) ψ)
26 nfv 1418 . . 3 u((x A y B) ψ)
27 nfv 1418 . . . 4 x(𝑡 A u B)
2827, 3nfan 1454 . . 3 x((𝑡 A u B) [𝑡 / x][u / y]ψ)
29 nfv 1418 . . . 4 y(𝑡 A u B)
3013nfsb 1819 . . . 4 y[𝑡 / x][u / y]ψ
3129, 30nfan 1454 . . 3 y((𝑡 A u B) [𝑡 / x][u / y]ψ)
32 eleq1 2097 . . . . 5 (x = 𝑡 → (x A𝑡 A))
33 eleq1 2097 . . . . 5 (y = u → (y Bu B))
3432, 33bi2anan9 538 . . . 4 ((x = 𝑡 y = u) → ((x A y B) ↔ (𝑡 A u B)))
3518, 8sylan9bbr 436 . . . 4 ((x = 𝑡 y = u) → (ψ ↔ [𝑡 / x][u / y]ψ))
3634, 35anbi12d 442 . . 3 ((x = 𝑡 y = u) → (((x A y B) ψ) ↔ ((𝑡 A u B) [𝑡 / x][u / y]ψ)))
3725, 26, 28, 31, 36cbvoprab12 5517 . 2 {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) ψ)} = {⟨⟨𝑡, u⟩, z⟩ ∣ ((𝑡 A u B) [𝑡 / x][u / y]ψ)}
3824, 37eqtr4i 2060 1 {⟨w, z⟩ ∣ (w (A × B) φ)} = {⟨⟨x, y⟩, z⟩ ∣ ((x A y B) ψ)}
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242  wnf 1346   wcel 1390  [wsb 1642  cop 3369  {copab 3807   × cxp 4285  {coprab 5453
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-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-v 2553  df-sbc 2759  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-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-iota 4809  df-fun 4846  df-fn 4847  df-f 4848  df-fo 4850  df-fv 4852  df-oprab 5456  df-1st 5706  df-2nd 5707
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator