![]() |
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 2427 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 1407 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfralxy.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfralxy.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfraldxy 2421 | . 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑) |
7 | 6 | mptru 1305 | 1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: ⊤wtru 1297 Ⅎwnf 1401 Ⅎwnfc 2222 ∀wral 2370 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 |
This theorem is referenced by: nfra2xy 2429 rspc2 2746 sbcralt 2929 sbcralg 2931 raaanlem 3407 nfint 3720 nfiinxy 3779 nfpo 4152 nfso 4153 nfse 4192 nffrfor 4199 nfwe 4206 ralxpf 4613 funimaexglem 5131 fun11iun 5309 dff13f 5587 nfiso 5623 mpt2eq123 5746 nfofr 5900 fmpt2x 6008 nfrecs 6110 xpf1o 6640 ac6sfi 6694 lble 8505 fzrevral 9668 nfsum1 10915 nfsum 10916 fsum2dlemstep 10993 fisumcom2 10997 bezoutlemmain 11430 setindis 12586 bdsetindis 12588 |
Copyright terms: Public domain | W3C validator |