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

Theorem opelopabsb 3988
Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
Assertion
Ref Expression
opelopabsb (⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ)
Distinct variable groups:   x,y   x,B
Allowed substitution hints:   φ(x,y)   A(x,y)   B(y)

Proof of Theorem opelopabsb
Dummy variables v u z w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elopab 3986 . . . 4 (⟨A, B {⟨u, v⟩ ∣ [u / x][v / y]φ} ↔ uv(⟨A, B⟩ = ⟨u, v [u / x][v / y]φ))
2 simpl 102 . . . . . . . 8 ((⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → ⟨A, B⟩ = ⟨u, v⟩)
32eqcomd 2042 . . . . . . 7 ((⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → ⟨u, v⟩ = ⟨A, B⟩)
4 vex 2554 . . . . . . . 8 u V
5 vex 2554 . . . . . . . 8 v V
64, 5opth 3965 . . . . . . 7 (⟨u, v⟩ = ⟨A, B⟩ ↔ (u = A v = B))
73, 6sylib 127 . . . . . 6 ((⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → (u = A v = B))
872eximi 1489 . . . . 5 (uv(⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → uv(u = A v = B))
9 eeanv 1804 . . . . . 6 (uv(u = A v = B) ↔ (u u = A v v = B))
10 isset 2555 . . . . . . 7 (A V ↔ u u = A)
11 isset 2555 . . . . . . 7 (B V ↔ v v = B)
1210, 11anbi12i 433 . . . . . 6 ((A V B V) ↔ (u u = A v v = B))
139, 12bitr4i 176 . . . . 5 (uv(u = A v = B) ↔ (A V B V))
148, 13sylib 127 . . . 4 (uv(⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → (A V B V))
151, 14sylbi 114 . . 3 (⟨A, B {⟨u, v⟩ ∣ [u / x][v / y]φ} → (A V B V))
16 nfv 1418 . . . 4 uφ
17 nfv 1418 . . . 4 vφ
18 nfs1v 1812 . . . 4 x[u / x][v / y]φ
19 nfs1v 1812 . . . . 5 y[v / y]φ
2019nfsbxy 1815 . . . 4 y[u / x][v / y]φ
21 sbequ12 1651 . . . . 5 (y = v → (φ ↔ [v / y]φ))
22 sbequ12 1651 . . . . 5 (x = u → ([v / y]φ ↔ [u / x][v / y]φ))
2321, 22sylan9bbr 436 . . . 4 ((x = u y = v) → (φ ↔ [u / x][v / y]φ))
2416, 17, 18, 20, 23cbvopab 3819 . . 3 {⟨x, y⟩ ∣ φ} = {⟨u, v⟩ ∣ [u / x][v / y]φ}
2515, 24eleq2s 2129 . 2 (⟨A, B {⟨x, y⟩ ∣ φ} → (A V B V))
26 sbcex 2766 . . 3 ([A / x][B / y]φA V)
27 spesbc 2837 . . . 4 ([A / x][B / y]φx[B / y]φ)
28 sbcex 2766 . . . . 5 ([B / y]φB V)
2928exlimiv 1486 . . . 4 (x[B / y]φB V)
3027, 29syl 14 . . 3 ([A / x][B / y]φB V)
3126, 30jca 290 . 2 ([A / x][B / y]φ → (A V B V))
32 opeq1 3540 . . . . 5 (z = A → ⟨z, w⟩ = ⟨A, w⟩)
3332eleq1d 2103 . . . 4 (z = A → (⟨z, w {⟨x, y⟩ ∣ φ} ↔ ⟨A, w {⟨x, y⟩ ∣ φ}))
34 dfsbcq2 2761 . . . 4 (z = A → ([z / x][w / y]φ[A / x][w / y]φ))
3533, 34bibi12d 224 . . 3 (z = A → ((⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ) ↔ (⟨A, w {⟨x, y⟩ ∣ φ} ↔ [A / x][w / y]φ)))
36 opeq2 3541 . . . . 5 (w = B → ⟨A, w⟩ = ⟨A, B⟩)
3736eleq1d 2103 . . . 4 (w = B → (⟨A, w {⟨x, y⟩ ∣ φ} ↔ ⟨A, B {⟨x, y⟩ ∣ φ}))
38 dfsbcq2 2761 . . . . 5 (w = B → ([w / y]φ[B / y]φ))
3938sbcbidv 2811 . . . 4 (w = B → ([A / x][w / y]φ[A / x][B / y]φ))
4037, 39bibi12d 224 . . 3 (w = B → ((⟨A, w {⟨x, y⟩ ∣ φ} ↔ [A / x][w / y]φ) ↔ (⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ)))
41 nfopab1 3817 . . . . . 6 x{⟨x, y⟩ ∣ φ}
4241nfel2 2187 . . . . 5 xz, w {⟨x, y⟩ ∣ φ}
43 nfs1v 1812 . . . . 5 x[z / x][w / y]φ
4442, 43nfbi 1478 . . . 4 x(⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)
45 opeq1 3540 . . . . . 6 (x = z → ⟨x, w⟩ = ⟨z, w⟩)
4645eleq1d 2103 . . . . 5 (x = z → (⟨x, w {⟨x, y⟩ ∣ φ} ↔ ⟨z, w {⟨x, y⟩ ∣ φ}))
47 sbequ12 1651 . . . . 5 (x = z → ([w / y]φ ↔ [z / x][w / y]φ))
4846, 47bibi12d 224 . . . 4 (x = z → ((⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ) ↔ (⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)))
49 nfopab2 3818 . . . . . . 7 y{⟨x, y⟩ ∣ φ}
5049nfel2 2187 . . . . . 6 yx, w {⟨x, y⟩ ∣ φ}
51 nfs1v 1812 . . . . . 6 y[w / y]φ
5250, 51nfbi 1478 . . . . 5 y(⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)
53 opeq2 3541 . . . . . . 7 (y = w → ⟨x, y⟩ = ⟨x, w⟩)
5453eleq1d 2103 . . . . . 6 (y = w → (⟨x, y {⟨x, y⟩ ∣ φ} ↔ ⟨x, w {⟨x, y⟩ ∣ φ}))
55 sbequ12 1651 . . . . . 6 (y = w → (φ ↔ [w / y]φ))
5654, 55bibi12d 224 . . . . 5 (y = w → ((⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ) ↔ (⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)))
57 opabid 3985 . . . . 5 (⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ)
5852, 56, 57chvar 1637 . . . 4 (⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)
5944, 48, 58chvar 1637 . . 3 (⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)
6035, 40, 59vtocl2g 2611 . 2 ((A V B V) → (⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ))
6125, 31, 60pm5.21nii 619 1 (⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ)
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = wceq 1242  wex 1378   wcel 1390  [wsb 1642  Vcvv 2551  [wsbc 2758  cop 3370  {copab 3808
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-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
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-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810
This theorem is referenced by:  brabsb  3989  opelopabaf  4001  opelopabf  4002  difopab  4412  isarep1  4928
  Copyright terms: Public domain W3C validator