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

Theorem nfraldya 2336
Description: Not-free for restricted universal quantification where y and A are distinct. See nfraldxy 2334 for a version with x and y distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
Hypotheses
Ref Expression
nfraldya.2 yφ
nfraldya.3 (φxA)
nfraldya.4 (φ → Ⅎxψ)
Assertion
Ref Expression
nfraldya (φ → Ⅎxy A ψ)
Distinct variable group:   y,A
Allowed substitution hints:   φ(x,y)   ψ(x,y)   A(x)

Proof of Theorem nfraldya
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 df-ral 2289 . 2 (y A ψy(y Aψ))
2 sbim 1809 . . . . . 6 ([z / y](y Aψ) ↔ ([z / y]y A → [z / y]ψ))
3 clelsb3 2124 . . . . . . 7 ([z / y]y Az A)
43imbi1i 227 . . . . . 6 (([z / y]y A → [z / y]ψ) ↔ (z A → [z / y]ψ))
52, 4bitri 173 . . . . 5 ([z / y](y Aψ) ↔ (z A → [z / y]ψ))
65albii 1339 . . . 4 (z[z / y](y Aψ) ↔ z(z A → [z / y]ψ))
7 nfv 1402 . . . . 5 z(y Aψ)
87sb8 1718 . . . 4 (y(y Aψ) ↔ z[z / y](y Aψ))
9 df-ral 2289 . . . 4 (z A [z / y]ψz(z A → [z / y]ψ))
106, 8, 93bitr4i 201 . . 3 (y(y Aψ) ↔ z A [z / y]ψ)
11 nfv 1402 . . . 4 zφ
12 nfraldya.3 . . . 4 (φxA)
13 nfraldya.2 . . . . 5 yφ
14 nfraldya.4 . . . . 5 (φ → Ⅎxψ)
1513, 14nfsbd 1833 . . . 4 (φ → Ⅎx[z / y]ψ)
1611, 12, 15nfraldxy 2334 . . 3 (φ → Ⅎxz A [z / y]ψ)
1710, 16nfxfrd 1344 . 2 (φ → Ⅎxy(y Aψ))
181, 17nfxfrd 1344 1 (φ → Ⅎxy A ψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226  wnf 1329   wcel 1374  [wsb 1627  wnfc 2147  wral 2284
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-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289
This theorem is referenced by:  nfralya  2340
  Copyright terms: Public domain W3C validator