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

Theorem nfiotadw 5182
Description: Bound-variable hypothesis builder for the class. (Contributed by Jim Kingdon, 21-Dec-2018.)
Hypotheses
Ref Expression
nfiotadw.1 𝑦𝜑
nfiotadw.2 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfiotadw (𝜑𝑥(℩𝑦𝜓))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem nfiotadw
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 dfiota2 5180 . 2 (℩𝑦𝜓) = {𝑧 ∣ ∀𝑦(𝜓𝑦 = 𝑧)}
2 nfv 1528 . . . 4 𝑧𝜑
3 nfiotadw.1 . . . . 5 𝑦𝜑
4 nfiotadw.2 . . . . . 6 (𝜑 → Ⅎ𝑥𝜓)
5 nfcv 2319 . . . . . . . 8 𝑥𝑦
6 nfcv 2319 . . . . . . . 8 𝑥𝑧
75, 6nfeq 2327 . . . . . . 7 𝑥 𝑦 = 𝑧
87a1i 9 . . . . . 6 (𝜑 → Ⅎ𝑥 𝑦 = 𝑧)
94, 8nfbid 1588 . . . . 5 (𝜑 → Ⅎ𝑥(𝜓𝑦 = 𝑧))
103, 9nfald 1760 . . . 4 (𝜑 → Ⅎ𝑥𝑦(𝜓𝑦 = 𝑧))
112, 10nfabd 2339 . . 3 (𝜑𝑥{𝑧 ∣ ∀𝑦(𝜓𝑦 = 𝑧)})
1211nfunid 3817 . 2 (𝜑𝑥 {𝑧 ∣ ∀𝑦(𝜓𝑦 = 𝑧)})
131, 12nfcxfrd 2317 1 (𝜑𝑥(℩𝑦𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wal 1351   = wceq 1353  wnf 1460  {cab 2163  wnfc 2306   cuni 3810  cio 5177
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-sn 3599  df-uni 3811  df-iota 5179
This theorem is referenced by:  nfiotaw  5183  nfriotadxy  5839
  Copyright terms: Public domain W3C validator