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

Theorem opelopabsb 3951
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 3948 . . . 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 2028 . . . . . . 7 ((⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → ⟨u, v⟩ = ⟨A, B⟩)
4 vex 2537 . . . . . . . 8 u V
5 vex 2537 . . . . . . . 8 v V
64, 5opth 3927 . . . . . . 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 1476 . . . . 5 (uv(⟨A, B⟩ = ⟨u, v [u / x][v / y]φ) → uv(u = A v = B))
9 eeanv 1790 . . . . . 6 (uv(u = A v = B) ↔ (u u = A v v = B))
10 isset 2538 . . . . . . 7 (A V ↔ u u = A)
11 isset 2538 . . . . . . 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 1404 . . . 4 uφ
17 nfv 1404 . . . 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 1637 . . . . 5 (y = v → (φ ↔ [v / y]φ))
22 sbequ12 1637 . . . . 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 3781 . . 3 {⟨x, y⟩ ∣ φ} = {⟨u, v⟩ ∣ [u / x][v / y]φ}
2515, 24eleq2s 2115 . 2 (⟨A, B {⟨x, y⟩ ∣ φ} → (A V B V))
26 sbcex 2748 . . 3 ([A / x][B / y]φA V)
27 spesbc 2820 . . . 4 ([A / x][B / y]φx[B / y]φ)
28 sbcex 2748 . . . . 5 ([B / y]φB V)
2928exlimiv 1473 . . . 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 3502 . . . . 5 (z = A → ⟨z, w⟩ = ⟨A, w⟩)
3332eleq1d 2089 . . . 4 (z = A → (⟨z, w {⟨x, y⟩ ∣ φ} ↔ ⟨A, w {⟨x, y⟩ ∣ φ}))
34 dfsbcq2 2743 . . . 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 3503 . . . . 5 (w = B → ⟨A, w⟩ = ⟨A, B⟩)
3736eleq1d 2089 . . . 4 (w = B → (⟨A, w {⟨x, y⟩ ∣ φ} ↔ ⟨A, B {⟨x, y⟩ ∣ φ}))
38 dfsbcq2 2743 . . . . 5 (w = B → ([w / y]φ[B / y]φ))
3938sbcbidv 2793 . . . 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 3779 . . . . . 6 x{⟨x, y⟩ ∣ φ}
4241nfel2 2173 . . . . 5 xz, w {⟨x, y⟩ ∣ φ}
43 nfs1v 1797 . . . . 5 x[z / x][w / y]φ
4442, 43nfbi 1465 . . . 4 x(⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)
45 opeq1 3502 . . . . . 6 (x = z → ⟨x, w⟩ = ⟨z, w⟩)
4645eleq1d 2089 . . . . 5 (x = z → (⟨x, w {⟨x, y⟩ ∣ φ} ↔ ⟨z, w {⟨x, y⟩ ∣ φ}))
47 sbequ12 1637 . . . . 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 3780 . . . . . . 7 y{⟨x, y⟩ ∣ φ}
5049nfel2 2173 . . . . . 6 yx, w {⟨x, y⟩ ∣ φ}
51 nfs1v 1797 . . . . . 6 y[w / y]φ
5250, 51nfbi 1465 . . . . 5 y(⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)
53 opeq2 3503 . . . . . . 7 (y = w → ⟨x, y⟩ = ⟨x, w⟩)
5453eleq1d 2089 . . . . . 6 (y = w → (⟨x, y {⟨x, y⟩ ∣ φ} ↔ ⟨x, w {⟨x, y⟩ ∣ φ}))
55 sbequ12 1637 . . . . . 6 (y = w → (φ ↔ [w / y]φ))
5654, 55bibi12d 224 . . . . 5 (y = w → ((⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ) ↔ (⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)))
57 opabid 3947 . . . . 5 (⟨x, y {⟨x, y⟩ ∣ φ} ↔ φ)
5852, 56, 57chvar 1623 . . . 4 (⟨x, w {⟨x, y⟩ ∣ φ} ↔ [w / y]φ)
5944, 48, 58chvar 1623 . . 3 (⟨z, w {⟨x, y⟩ ∣ φ} ↔ [z / x][w / y]φ)
6035, 40, 59vtocl2g 2593 . 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  wex 1362   = wceq 1374   wcel 1376  [wsb 1628  Vcvv 2534  [wsbc 2740  cop 3331  {copab 3770
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 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-14 1388  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2005  ax-sep 3828  ax-pow 3880  ax-pr 3897
This theorem depends on definitions:  df-bi 110  df-3an 878  df-tru 1232  df-nf 1330  df-sb 1629  df-eu 1885  df-mo 1886  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-rex 2289  df-v 2536  df-sbc 2741  df-un 2901  df-in 2903  df-ss 2910  df-pw 3314  df-sn 3334  df-pr 3335  df-op 3337  df-opab 3772
This theorem is referenced by:  brabsb  3952  opelopabaf  3964  opelopabf  3965  difopab  4372  isarep1  4888
  Copyright terms: Public domain W3C validator