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

Theorem opelopabsb 3971
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 3969 . . . 4 (⟨A, B {⟨u, v⟩ ∣ [u / x][v / y]φ} ↔ uv(⟨A, B⟩ = ⟨u, v [u / x][v / y]φ))
2 ax-ia1 99 . . . . . . . 8 ((⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → ⟨A, B⟩ = ⟨u, v⟩)
32eqcomd 2027 . . . . . . 7 ((⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → ⟨u, v⟩ = ⟨A, B⟩)
4 vex 2538 . . . . . . . 8 u V
5 vex 2538 . . . . . . . 8 v V
64, 5opth 3948 . . . . . . 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 1474 . . . . 5 (uv(⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → uv(u = A v = B))
9 eeanv 1789 . . . . . 6 (uv(u = A v = B) ↔ (u u = A v v = B))
10 isset 2539 . . . . . . 7 (A V ↔ u u = A)
11 isset 2539 . . . . . . 7 (B V ↔ v v = B)
1210, 11anbi12i 436 . . . . . 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 1402 . . . 4 uφ
17 nfv 1402 . . . 4 vφ
18 nfs1v 1797 . . . 4 x[u / x][v / y]φ
19 nfs1v 1797 . . . . 5 y[v / y]φ
2019nfsbxy 1800 . . . 4 y[u / x][v / y]φ
21 sbequ12 1636 . . . . 5 (y = v → (φ ↔ [v / y]φ))
22 sbequ12 1636 . . . . 5 (x = u → ([v / y]φ ↔ [u / x][v / y]φ))
2321, 22sylan9bbr 439 . . . 4 ((x = u y = v) → (φ ↔ [u / x][v / y]φ))
2416, 17, 18, 20, 23cbvopab 3802 . . 3 {⟨x, y⟩ ∣ φ} = {⟨u, v⟩ ∣ [u / x][v / y]φ}
2515, 24eleq2s 2114 . 2 (⟨A, B {⟨x, y⟩ ∣ φ} → (A V B V))
26 sbcex 2749 . . 3 ([A / x][B / y]φA V)
27 spesbc 2820 . . . 4 ([A / x][B / y]φx[B / y]φ)
28 sbcex 2749 . . . . 5 ([B / y]φB V)
2928exlimiv 1471 . . . 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 3523 . . . . 5 (z = A → ⟨z, w⟩ = ⟨A, w⟩)
3332eleq1d 2088 . . . 4 (z = A → (⟨z, w {⟨x, y⟩ ∣ φ} ↔ ⟨A, w {⟨x, y⟩ ∣ φ}))
34 dfsbcq2 2744 . . . 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 3524 . . . . 5 (w = B → ⟨A, w⟩ = ⟨A, B⟩)
3736eleq1d 2088 . . . 4 (w = B → (⟨A, w {⟨x, y⟩ ∣ φ} ↔ ⟨A, B {⟨x, y⟩ ∣ φ}))
38 dfsbcq2 2744 . . . . 5 (w = B → ([w / y]φ[B / y]φ))
3938sbcbidv 2794 . . . 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 3800 . . . . . 6 x{⟨x, y⟩ ∣ φ}
4241nfel2 2172 . . . . 5 xz, w {⟨x, y⟩ ∣ φ}
43 nfs1v 1797 . . . . 5 x[z / x][w / y]φ
4442, 43nfbi 1463 . . . 4 x(⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)
45 opeq1 3523 . . . . . 6 (x = z → ⟨x, w⟩ = ⟨z, w⟩)
4645eleq1d 2088 . . . . 5 (x = z → (⟨x, w {⟨x, y⟩ ∣ φ} ↔ ⟨z, w {⟨x, y⟩ ∣ φ}))
47 sbequ12 1636 . . . . 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 3801 . . . . . . 7 y{⟨x, y⟩ ∣ φ}
5049nfel2 2172 . . . . . 6 yx, w {⟨x, y⟩ ∣ φ}
51 nfs1v 1797 . . . . . 6 y[w / y]φ
5250, 51nfbi 1463 . . . . 5 y(⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)
53 opeq2 3524 . . . . . . 7 (y = w → ⟨x, y⟩ = ⟨x, w⟩)
5453eleq1d 2088 . . . . . 6 (y = w → (⟨x, y {⟨x, y⟩ ∣ φ} ↔ ⟨x, w {⟨x, y⟩ ∣ φ}))
55 sbequ12 1636 . . . . . 6 (y = w → (φ ↔ [w / y]φ))
5654, 55bibi12d 224 . . . . 5 (y = w → ((⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ) ↔ (⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)))
57 opabid 3968 . . . . 5 (⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ)
5852, 56, 57chvar 1622 . . . 4 (⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)
5944, 48, 58chvar 1622 . . 3 (⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)
6035, 40, 59vtocl2g 2594 . 2 ((A V B V) → (⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ))
6125, 31, 60pm5.21nii 607 1 (⟨A, B {⟨x, y⟩ ∣ φ} ↔ [A / x][B / y]φ)
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = wceq 1228  wex 1362   wcel 1374  [wsb 1627  Vcvv 2535  [wsbc 2741  cop 3353  {copab 3791
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 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-rex 2290  df-v 2537  df-sbc 2742  df-un 2899  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-opab 3793
This theorem is referenced by:  brabsb  3972  opelopabaf  3984  opelopabf  3985  difopab  4396  isarep1  4911
  Copyright terms: Public domain W3C validator