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 2362 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 1355 | . . 3 ⊢ Ⅎ𝑦⊤ | |
2 | nfralxy.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝐴) |
4 | nfralxy.2 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
5 | 4 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
6 | 1, 3, 5 | nfraldxy 2356 | . 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑) |
7 | 6 | trud 1252 | 1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: ⊤wtru 1244 Ⅎwnf 1349 Ⅎwnfc 2165 ∀wral 2306 |
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-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ral 2311 |
This theorem is referenced by: nfra2xy 2364 rspc2 2661 sbcralt 2834 sbcralg 2836 raaanlem 3326 nfint 3625 nfiinxy 3684 nfpo 4038 nfso 4039 nfse 4078 nffrfor 4085 nfwe 4092 ralxpf 4482 funimaexglem 4982 fun11iun 5147 dff13f 5409 nfiso 5446 mpt2eq123 5564 fmpt2x 5826 nfrecs 5922 ac6sfi 6352 fzrevral 8967 setindis 10092 bdsetindis 10094 |
Copyright terms: Public domain | W3C validator |