![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfralxy | GIF version |
Description: Not-free for restricted universal quantification where 𝑥 and 𝑦 are distinct. See nfralya 2410 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.) |
Ref | Expression |
---|---|
nfralxy.1 | ⊢ Ⅎ𝑥𝐴 |
nfralxy.2 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfralxy | ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1396 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfralxy.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfralxy.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfraldxy 2404 | . 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑) |
7 | 6 | trud 1294 | 1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: ⊤wtru 1286 Ⅎwnf 1390 Ⅎwnfc 2210 ∀wral 2353 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ral 2358 |
This theorem is referenced by: nfra2xy 2412 rspc2 2721 sbcralt 2901 sbcralg 2903 raaanlem 3368 nfint 3672 nfiinxy 3731 nfpo 4092 nfso 4093 nfse 4132 nffrfor 4139 nfwe 4146 ralxpf 4540 funimaexglem 5050 fun11iun 5222 dff13f 5489 nfiso 5525 mpt2eq123 5643 nfofr 5797 fmpt2x 5905 nfrecs 6004 xpf1o 6490 ac6sfi 6544 lble 8302 fzrevral 9412 nfsum1 10567 nfsum 10568 bezoutlemmain 10767 setindis 11205 bdsetindis 11207 |
Copyright terms: Public domain | W3C validator |